X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=README;h=3064ce64e3c8cfe1d64c984ce480f5191b0a6e6a;hp=e4a85bd84ef8d7f8c5c4d075770707046a36f15c;hb=074f97c4bb71c6d9851daec95eae14cf1c3bab25;hpb=299acd153fa357fbc31e2877a37d8eb9d64f309e

diff --git a/README b/README
index e4a85bd..3064ce6 100644
--- a/README
+++ b/README
@@ -136,6 +136,11 @@ 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
 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
 available to the dynamic linker, using the LD_LIBRARY_PATH environment