Add a DafnyCC option that disables some of Dafny's cleverness to better match DafnyCC's capabilities

1 files changed, 9 insertions, 0 deletions

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index f9146cca..8c36ece9 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -31,6 +31,7 @@ namespace Microsoft.Dafny
     }

 

     public bool DisallowSoundnessCheating = false;

+    public bool Dafnycc = false;

     public int Induction = 3;

     public int InductionHeuristic = 6;

     public string DafnyPrelude = null;

@@ -118,6 +119,13 @@ namespace Microsoft.Dafny
             return true;

           }

 

+        case "dafnycc":

+          Dafnycc = true;

+          Induction = 0;

+          Compile = false;

+          UseAbstractInterpretation = false; // /noinfer

+          return true;

+

         case "noCheating": {

             int cheat = 0; // 0 is default, allows cheating

             if (ps.GetNumericArgument(ref cheat, 2)) {

@@ -209,6 +217,7 @@ namespace Microsoft.Dafny
                 0 (default) - don't write the compiled Dafny program (but

                     still compile it, if /compile indicates to do so)

                 1 - write the compiled Dafny program as a .cs file

+  /dafnycc      Disable features not supported by DafnyCC

   /noCheating:<n>

                 0 (default) - allow assume statements and free invariants

                 1 - treat all assumptions as asserts, and drop free.