X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=README;h=3064ce64e3c8cfe1d64c984ce480f5191b0a6e6a;hp=89f9e24ba6976f2fb6ed4b80d94ab286a8e7ddb1;hb=074f97c4bb71c6d9851daec95eae14cf1c3bab25;hpb=16b2fd3b0f423ce6ed9fa878ed35eb2d68ff5934

diff --git a/README b/README
index 89f9e24..3064ce6 100644
--- a/README
+++ b/README
@@ -4,7 +4,7 @@
 
 Copyright (c) 2013 Regents of the University of California. All rights reserved.
 
-CDSChecker is distributed under the GPL v2.
+CDSChecker is distributed under the GPL v2. See the LICENSE file for details.
 
 This README is divided into sections as follows:
 
@@ -90,7 +90,9 @@ Model-checker options:
                               Default: 1
 -b, --bound=MAX             Upper length bound.
                               Default: 0
--v, --verbose               Print verbose execution information.
+-v[NUM], --verbose[=NUM]    Print verbose execution information. NUM is optional:
+                              0 is quiet; 1 is noisy; 2 is noisier.
+                              Default: 0
 -u, --uninitialized=VALUE   Return VALUE any load which may read from an
                               uninitialized atomic.
                               Default: 0
@@ -99,6 +101,9 @@ Model-checker options:
                             -o help for a list of options
  --                         Program arguments follow.
 
+Analysis plugins:
+SC
+
 
 Note that we also provide a series of benchmarks (distributed separately),
 which can be placed under the benchmarks/ directory. After building CDSChecker,
@@ -129,7 +134,12 @@ We only support C11 thread syntax (thrd_t, etc. from <thread.h>).
 Test programs may also use our included happens-before race detector by
 including <librace.h> and utilizing the appropriate functions
 (store_{8,16,32,64}() and load_{8,16,32,64}()) for loading/storing data from/to
-from non-atomic shared memory.
+non-atomic shared memory.
+
+CDSChecker can also check boolean assertions in your test programs. Just
+include <model-assert.h> and use the MODEL_ASSERT() macro in your test program.
+CDSChecker will report a bug in any possible execution in which the argument to
+MODEL_ASSERT() evaluates to false (that is, 0).
 
 Test programs should be compiled against our shared library (libmodel.so) using
 the headers in the include/ directory. Then the shared library must be made