Ensure that no file is processed twice, even if one command-line file is included by another command-line file.

2 files changed, 6 insertions, 3 deletions

diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
index 34b509a0..7c522bd8 100644
--- a/Source/Dafny/DafnyMain.cs
+++ b/Source/Dafny/DafnyMain.cs
@@ -54,7 +54,7 @@ namespace Microsoft.Dafny {
       }

 

       if (!DafnyOptions.O.DisallowIncludes) {

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

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

         if (errString != null) {

           return errString;

         }

@@ -84,8 +84,11 @@ namespace Microsoft.Dafny {
       }

     }

 

-    public static string ParseIncludes(ModuleDecl module, BuiltIns builtIns, Errors errs) {

+    public static string ParseIncludes(ModuleDecl module, BuiltIns builtIns, List<string> excludeFiles, Errors errs) {

       SortedSet<Include> includes = new SortedSet<Include>(new IncludeComparer());

+      foreach (string fileName in excludeFiles) {

+        includes.Add(new Include(null, fileName, Path.GetFullPath(fileName)));

+      }

       bool newlyIncluded;

       do {

         newlyIncluded = false;

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index e96e0743..9bfdaae7 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -99,7 +99,7 @@ namespace DafnyLanguage
       Dafny.BuiltIns builtIns = new Dafny.BuiltIns();

       Dafny.Errors parseErrors = new VSErrors(this);

       int errorCount = Dafny.Parser.Parse(_snapshot.GetText(), _filename, module, builtIns, parseErrors);

-      string errString = Dafny.Main.ParseIncludes(module, builtIns, parseErrors);

+      string errString = Dafny.Main.ParseIncludes(module, builtIns, new List<string>(), parseErrors);

       if (errorCount != 0 || errString != null)

         return false;

       Dafny.Program program = new Dafny.Program(_filename, module, builtIns);