diff options
Diffstat (limited to 'Source/Core/CommandLineOptions.ssc')
| -rw-r--r-- | Source/Core/CommandLineOptions.ssc | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index 5912220d..aa07ec41 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -159,6 +159,7 @@ namespace Microsoft.Boogie public enum VCVariety { Structured, Block, Local, BlockNested, BlockReach, BlockNestedReach, Dag, Doomed, Unspecified }
public VCVariety vcVariety = VCVariety.Unspecified; // will not be Unspecified after command line has been parsed
+ public bool useDoomDebug = false; // Will use doomed analysis to search for errors if set
public bool RemoveEmptyBlocks = true;
@@ -819,7 +820,12 @@ namespace Microsoft.Boogie }
}
break;
-
+
+ case "/DoomDebug":
+ vcVariety = VCVariety.Doomed;
+ useDoomDebug = true;
+ break;
+
case "-vc":
case "/vc":
if (ps.ConfirmArgumentCount(1)) {
@@ -1818,6 +1824,7 @@ namespace Microsoft.Boogie b = flat block, r = flat block reach,
s = structured, l = local, d = dag (default with /prover:z3)
doomed = doomed
+ /DoomDebug : Use Doom detection to debug (experimental)
/traceverify : print debug output during verification condition generation
/subsumption:<c> : apply subsumption to asserted conditions:
0 - never, 1 - not for quantifiers, 2 (default) - always
|