Add a command-line option to disable include directives.

2 files changed, 12 insertions, 4 deletions

diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
index 17532fa9..182567d9 100644
--- a/Source/Dafny/DafnyMain.cs
+++ b/Source/Dafny/DafnyMain.cs
@@ -38,10 +38,12 @@ namespace Microsoft.Dafny {
         }        

       }

 

-      string errString = ParseIncludes(module, builtIns, new Errors());

-      if (errString != null) {

-        return errString;

-      } 

+      if (!DafnyOptions.O.DisallowIncludes) {

+        string errString = ParseIncludes(module, builtIns, new Errors());

+        if (errString != null) {

+          return errString;

+        }

+      }

 

       program = new Program(programName, module, builtIns);

 

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

     }