Add a command-line option to disable include directives.

1 files changed, 6 insertions, 0 deletions

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 9176b8e1..753fbb32 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -39,6 +39,7 @@ namespace Microsoft.Dafny
     public bool Compile = true;

     public bool ForceCompile = false;

     public bool SpillTargetCode = false;

+    public bool DisallowIncludes = false;

 

     protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {

       var args = ps.args;  // convenient synonym

@@ -96,6 +97,10 @@ namespace Microsoft.Dafny
           ps.GetNumericArgument(ref InductionHeuristic, 7);

           return true;

 

+        case "noInclude":

+          DisallowIncludes = true;

+          return true;

+

         default:

           break;

       }

@@ -154,6 +159,7 @@ namespace Microsoft.Dafny
                 1,2,3,4,5 - levels in between, ordered as follows as far as

                     how discriminating they are:  0 < 1 < 2 < (3,4) < 5 < 6

                 6 (default) - most discriminating

+  /noIncludes   Ignore include directives

 ");

       base.Usage();  // also print the Boogie options

     }