Added experimental feature /DoomDebug. Can be test using Test/doomed/doomdebug.bpl

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