Fix a bug with includes and /useBaseNameForFileName

If /useBasenameForFilename is specified, tokens just contain file names, which
is not enough to locate included files.

Solution based on Rustan's advice.

1 files changed, 8 insertions, 8 deletions

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index d50a4dd6..dae1b95e 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -112,11 +112,11 @@ public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns built
   string s;

   if (filename == "stdin.dfy") {

     s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string>());

-    return Parse(s, filename, module, builtIns, errors, verifyThisFile);

+    return Parse(s, filename, filename, module, builtIns, errors, verifyThisFile);

   } else {

     using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {

       s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string>());

-      return Parse(s, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, module, builtIns, errors, verifyThisFile);

+      return Parse(s, filename, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, module, builtIns, errors, verifyThisFile);

     }

   }

 }

@@ -126,12 +126,12 @@ public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns built
 /// Returns the number of parsing errors encountered.

 /// Note: first initialize the Scanner.

 ///</summary>

-public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true) {

+public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true) {

   Contract.Requires(s != null);

   Contract.Requires(filename != null);

   Contract.Requires(module != null);

   Errors errors = new Errors();

-  return Parse(s, filename, module, builtIns, errors, verifyThisFile);

+  return Parse(s, fullFilename, filename, module, builtIns, errors, verifyThisFile);

 }

 ///<summary>

 /// Parses top-level things (modules, classes, datatypes, class members)

@@ -139,15 +139,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module,
 /// Returns the number of parsing errors encountered.

 /// Note: first initialize the Scanner with the given Errors sink.

 ///</summary>

-public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns,

-                         Errors/*!*/ errors, bool verifyThisFile=true) {

+public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ filename, ModuleDecl module,

+                         BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) {

   Contract.Requires(s != null);

   Contract.Requires(filename != null);

   Contract.Requires(module != null);

   Contract.Requires(errors != null);

   byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));

   MemoryStream ms = new MemoryStream(buffer,false);

-  Scanner scanner = new Scanner(ms, errors, filename);

+  Scanner scanner = new Scanner(ms, errors, fullFilename, filename);

   Parser parser = new Parser(scanner, errors, module, builtIns, verifyThisFile);

   parser.Parse();

   return parser.errors.count;

@@ -536,7 +536,7 @@ bool IsType(ref IToken pt) {
 			Get();

 			Expect(20);

 			{

-			 string parsedFile = t.filename;

+			 string parsedFile = scanner.FullFilename;

 			 bool isVerbatimString;

 			 string includedFile = Util.RemoveParsedStringQuotes(t.val, out isVerbatimString);

 			 includedFile = Util.RemoveEscaping(includedFile, isVerbatimString);