summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2011-01-13 02:46:19 +0000
committerGravatar MichalMoskal <unknown>2011-01-13 02:46:19 +0000
commitc6c815a8ddb80eb4e43714a6223bd8e5c7687a74 (patch)
treeb14da00fa49b87400a7dc56b43ff0e6a81ac31a2 /Test
parentfc7f866729720fab4451f90f53827625fa3fa631 (diff)
Add description of {:selective_checking} to the /attrHelp. Fix the testcase.
Diffstat (limited to 'Test')
-rw-r--r--Test/test2/SelectiveChecking.bpl8
1 files changed, 0 insertions, 8 deletions
diff --git a/Test/test2/SelectiveChecking.bpl b/Test/test2/SelectiveChecking.bpl
index 2f08618a..ed40787e 100644
--- a/Test/test2/SelectiveChecking.bpl
+++ b/Test/test2/SelectiveChecking.bpl
@@ -1,11 +1,3 @@
-/*
-In functions marked with {:selective_checking} all asserts are turned into assumes,
-except for the ones reachable from the commands marked with {:start_checking_here}.
-Thus, "assume {:start_checking_here} whatever;" is an inverse of "assume false;".
-The first one disables all verification before it, and the second one disables
-all verification after.
-*/
-
procedure {:selective_checking} foo()
{
var x, y, z : int;