diff options
-rw-r--r-- | Source/Core/CommandLineOptions.cs | 7 | ||||
-rw-r--r-- | Test/test2/SelectiveChecking.bpl | 8 |
2 files changed, 7 insertions, 8 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 11406dbc..5feff30a 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1906,6 +1906,13 @@ namespace Microsoft.Boogie { Per-implementation versions of
/vcsMaxCost, /vcsMaxSplits and /vcsMaxKeepGoingSplits.
+ {:selective_checking true}
+ Turn all asserts into assumes except for the ones reachable from
+ assumptions marked with the attribute {:start_checking_here}.
+ Thus, ""assume {:start_checking_here} something;"" becomes an inverse
+ of ""assume false;"": the first one disables all verification before
+ it, and the second one disables all verification after.
+
---- On functions ----------------------------------------------------------
{:bvbuiltin ""spec""}
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; |