Add description of {:selective_checking} to the /attrHelp. Fix the testcase.

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;