Fixed issues with absolute file names in the expected output for the lit tests.

5 files changed, 28 insertions, 11 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index e7b36227..93e39ae6 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -15,11 +15,11 @@ namespace Microsoft.Dafny {
   public class Program {

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(Name != null);

+      Contract.Invariant(FullName != null);

       Contract.Invariant(DefaultModule != null);

     }

 

-    public readonly string Name;

+    public readonly string FullName;

     public List<ModuleDefinition> Modules; // filled in during resolution.

                                                      // Resolution essentially flattens the module hierarchy, for

                                                      // purposes of translation and compilation.

@@ -36,7 +36,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(name != null);

       Contract.Requires(module != null);

       Contract.Requires(module is LiteralModuleDecl);

-      Name = name;

+      FullName = name;

       DefaultModule = module;

       DefaultModuleDef = (DefaultModuleDecl)((LiteralModuleDecl)module).ModuleDef;

       BuiltIns = builtIns;

@@ -44,6 +44,21 @@ namespace Microsoft.Dafny {
       CompileModules = new List<ModuleDefinition>();

       TranslationTasks = new List<TranslationTask>();

     }

+

+    public string Name

+    {

+      get

+      {

+        try

+        {

+          return System.IO.Path.GetFileName(FullName);

+        }

+        catch (ArgumentException)

+        {

+          return FullName;

+        }

+      }

+    }

   }

 

   public class Include : IComparable

diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
index f604ebe6..60578e33 100644
--- a/Source/Dafny/DafnyMain.cs
+++ b/Source/Dafny/DafnyMain.cs
@@ -77,7 +77,7 @@ namespace Microsoft.Dafny {
         }

       }

       if (r.ErrorCount != 0) {

-        return string.Format("{0} resolution/type errors detected in {1}", r.ErrorCount, programName);

+        return string.Format("{0} resolution/type errors detected in {1}", r.ErrorCount, program.Name);

       }

 

       return null;  // success

@@ -117,14 +117,15 @@ namespace Microsoft.Dafny {
     }

 

     private static string ParseFile(string dafnyFileName, Bpl.IToken tok, ModuleDecl module, BuiltIns builtIns, Errors errs, bool verifyThisFile = true) {

+      var fn = DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(dafnyFileName) : dafnyFileName;

       try {

         int errorCount = Dafny.Parser.Parse(dafnyFileName, module, builtIns, errs, verifyThisFile);

         if (errorCount != 0) {

-          return string.Format("{0} parse errors detected in {1}", errorCount, dafnyFileName);

+          return string.Format("{0} parse errors detected in {1}", errorCount, fn);

         }

       } catch (IOException e) {

         errs.SemErr(tok, "Unable to open included file");

-        return string.Format("Error opening file \"{0}\": {1}", dafnyFileName, e.Message);

+        return string.Format("Error opening file \"{0}\": {1}", fn, e.Message);

       }

       return null; // Success

     }

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 7d8c3fdb..f1eedbba 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -312,6 +312,7 @@ namespace Microsoft.Dafny
         cp.ReferencedAssemblies.Add("System.Numerics.dll");

 

         var cr = provider.CompileAssemblyFromSource(cp, csharpProgram);

+        var assemblyName = Path.GetFileName(cr.PathToAssembly);

         if (DafnyOptions.O.RunAfterCompile && cr.Errors.Count == 0) {

           outputWriter.WriteLine("Program compiled successfully");

           outputWriter.WriteLine("Running...");

@@ -327,9 +328,9 @@ namespace Microsoft.Dafny
             outputWriter.WriteLine(e.ToString());

           }

         } else if (cr.Errors.Count == 0) {

-          outputWriter.WriteLine("Compiled assembly into {0}", DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(cr.PathToAssembly) : cr.PathToAssembly);

+          outputWriter.WriteLine("Compiled assembly into {0}", assemblyName);

         } else {

-          outputWriter.WriteLine("Errors compiling program into {0}", DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(cr.PathToAssembly) : cr.PathToAssembly);

+          outputWriter.WriteLine("Errors compiling program into {0}", assemblyName);

           foreach (var ce in cr.Errors) {

             outputWriter.WriteLine(ce.ToString());

             outputWriter.WriteLine();

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 0f16242c..801e3ebd 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -173,7 +173,7 @@ namespace DafnyLanguage
     public static void Compile(Dafny.Program dafnyProgram, TextWriter outputWriter)

     {

       Microsoft.Dafny.DafnyOptions.O.SpillTargetCode = true;

-      Microsoft.Dafny.DafnyDriver.CompileDafnyProgram(dafnyProgram, dafnyProgram.Name, outputWriter);

+      Microsoft.Dafny.DafnyDriver.CompileDafnyProgram(dafnyProgram, dafnyProgram.FullName, outputWriter);

     }

 

     #endregion

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index 977ac4f0..3da47538 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -322,9 +322,9 @@ namespace DafnyLanguage
 

       if (_logSnapshots)

       {

-        var logDirName = System.IO.Path.Combine(System.IO.Path.GetDirectoryName(program.Name), "logs");

+        var logDirName = System.IO.Path.Combine(System.IO.Path.GetDirectoryName(program.FullName), "logs");

         Directory.CreateDirectory(logDirName);

-        var logFileName = System.IO.Path.Combine(logDirName, System.IO.Path.GetFileName(System.IO.Path.ChangeExtension(program.Name, string.Format("{0}.v{1}{2}", _created.Ticks, _version, System.IO.Path.GetExtension(program.Name)))));        

+        var logFileName = System.IO.Path.Combine(logDirName, System.IO.Path.GetFileName(System.IO.Path.ChangeExtension(program.FullName, string.Format("{0}.v{1}{2}", _created.Ticks, _version, System.IO.Path.GetExtension(program.FullName)))));        

         using (var writer = new StreamWriter(logFileName))

         {

           var pr = new Dafny.Printer(writer);