From 074f97c4bb71c6d9851daec95eae14cf1c3bab25 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Sat, 1 Jun 2013 16:08:16 -0700 Subject: [PATCH] README: add bit on MODEL_ASSERT() macro --- README | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/README b/README index e4a85bd..3064ce6 100644 --- a/README +++ b/README @@ -136,6 +136,11 @@ including 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 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 -- 2.34.1