diff options
Diffstat (limited to 'Test/test2')
| -rw-r--r-- | Test/test2/SelectiveChecking.bpl | 8 |
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; |