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

24 files changed, 47 insertions, 30 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);

diff --git a/Test/dafny0/AssumptionVariables0.dfy.expect b/Test/dafny0/AssumptionVariables0.dfy.expect
index 914d83eb..f2d43fe1 100644
--- a/Test/dafny0/AssumptionVariables0.dfy.expect
+++ b/Test/dafny0/AssumptionVariables0.dfy.expect
@@ -11,4 +11,4 @@ AssumptionVariables0.dfy(57,26): Error: assumption variable must be ghost
 AssumptionVariables0.dfy(61,37): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

 AssumptionVariables0.dfy(61,10): Error: assumption variable must be of type 'bool'

 AssumptionVariables0.dfy(69,15): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

-13 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\AssumptionVariables0.dfy

+13 resolution/type errors detected in AssumptionVariables0.dfy

diff --git a/Test/dafny0/CallStmtTests.dfy.expect b/Test/dafny0/CallStmtTests.dfy.expect
index 329a702f..57a33c62 100644
--- a/Test/dafny0/CallStmtTests.dfy.expect
+++ b/Test/dafny0/CallStmtTests.dfy.expect
@@ -1,3 +1,3 @@
 CallStmtTests.dfy(6,3): Error: LHS of assignment must denote a mutable variable

 CallStmtTests.dfy(17,8): Error: actual out-parameter 0 is required to be a ghost variable

-2 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\CallStmtTests.dfy

+2 resolution/type errors detected in CallStmtTests.dfy

diff --git a/Test/dafny0/CoResolution.dfy.expect b/Test/dafny0/CoResolution.dfy.expect
index 423bf928..e9022f41 100644
--- a/Test/dafny0/CoResolution.dfy.expect
+++ b/Test/dafny0/CoResolution.dfy.expect
@@ -19,4 +19,4 @@ CoResolution.dfy(141,17): Error: a recursive call from a copredicate can go only
 CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

-21 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\CoResolution.dfy

+21 resolution/type errors detected in CoResolution.dfy

diff --git a/Test/dafny0/Coinductive.dfy.expect b/Test/dafny0/Coinductive.dfy.expect
index ccb24b72..ce3e3a8d 100644
--- a/Test/dafny0/Coinductive.dfy.expect
+++ b/Test/dafny0/Coinductive.dfy.expect
@@ -14,4 +14,4 @@ Coinductive.dfy(116,24): Error: a copredicate can be called recursively only in
 Coinductive.dfy(122,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

 Coinductive.dfy(123,10): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

 Coinductive.dfy(148,5): Error: a recursive call from a copredicate can go only to other copredicates

-16 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\Coinductive.dfy

+16 resolution/type errors detected in Coinductive.dfy

diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect
index 4504b114..186c53be 100644
--- a/Test/dafny0/EqualityTypes.dfy.expect
+++ b/Test/dafny0/EqualityTypes.dfy.expect
@@ -9,4 +9,4 @@ EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must sup
 EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D)

 EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D)

 EqualityTypes.dfy(118,16): Error: == can only be applied to expressions of types that support equality (got D)

-11 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\EqualityTypes.dfy

+11 resolution/type errors detected in EqualityTypes.dfy

diff --git a/Test/dafny0/IteratorResolution.dfy.expect b/Test/dafny0/IteratorResolution.dfy.expect
index 25890cd9..b68882fa 100644
--- a/Test/dafny0/IteratorResolution.dfy.expect
+++ b/Test/dafny0/IteratorResolution.dfy.expect
@@ -10,4 +10,4 @@ IteratorResolution.dfy(127,21): Error: arguments must have the same type (got in
 IteratorResolution.dfy(128,2): Error: LHS of assignment must denote a mutable field

 IteratorResolution.dfy(135,9): Error: unresolved identifier: _decreases1

 IteratorResolution.dfy(140,9): Error: unresolved identifier: _decreases0

-12 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\IteratorResolution.dfy

+12 resolution/type errors detected in IteratorResolution.dfy

diff --git a/Test/dafny0/LiberalEquality.dfy.expect b/Test/dafny0/LiberalEquality.dfy.expect
index 1af19a3f..0b2cbb74 100644
--- a/Test/dafny0/LiberalEquality.dfy.expect
+++ b/Test/dafny0/LiberalEquality.dfy.expect
@@ -1,4 +1,4 @@
 LiberalEquality.dfy(20,14): Error: arguments must have the same type (got T and U)

 LiberalEquality.dfy(39,14): Error: arguments must have the same type (got Weird<T,int,V> and Weird<T,bool,V>)

 LiberalEquality.dfy(54,14): Error: arguments must have the same type (got array<int> and array<bool>)

-3 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\LiberalEquality.dfy

+3 resolution/type errors detected in LiberalEquality.dfy

diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect
index eaa422b3..3d8a5099 100644
--- a/Test/dafny0/Modules0.dfy.expect
+++ b/Test/dafny0/Modules0.dfy.expect
@@ -26,4 +26,4 @@ Modules0.dfy(288,16): Error: type of the receiver is not fully determined at thi
 Modules0.dfy(288,6): Error: expected method call, found expression

 Modules0.dfy(310,24): Error: module Q_Imp does not exist

 Modules0.dfy(100,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)

-28 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\Modules0.dfy

+28 resolution/type errors detected in Modules0.dfy

diff --git a/Test/dafny0/Modules2.dfy.expect b/Test/dafny0/Modules2.dfy.expect
index ed25001a..3d37146d 100644
--- a/Test/dafny0/Modules2.dfy.expect
+++ b/Test/dafny0/Modules2.dfy.expect
@@ -3,4 +3,4 @@ Modules2.dfy(46,10): Error: new can be applied only to reference types (got C)
 Modules2.dfy(49,14): Error: the name 'E' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'D.E')

 Modules2.dfy(50,14): Error: The name D ambiguously refers to a type in one of the modules A, B

 Modules2.dfy(52,11): Error: The name f ambiguously refers to a static member in one of the modules A, B

-5 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\Modules2.dfy

+5 resolution/type errors detected in Modules2.dfy

diff --git a/Test/dafny0/ModulesCycle.dfy.expect b/Test/dafny0/ModulesCycle.dfy.expect
index 516687e9..6f9cee45 100644
--- a/Test/dafny0/ModulesCycle.dfy.expect
+++ b/Test/dafny0/ModulesCycle.dfy.expect
@@ -1,3 +1,3 @@
 ModulesCycle.dfy(5,9): Error: module T does not exist

 ModulesCycle.dfy(8,7): Error: module definition contains a cycle (note: parent modules implicitly depend on submodules): A -> D -> C -> B

-2 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\ModulesCycle.dfy

+2 resolution/type errors detected in ModulesCycle.dfy

diff --git a/Test/dafny0/NonGhostQuantifiers.dfy.expect b/Test/dafny0/NonGhostQuantifiers.dfy.expect
index d290a1ab..1e2fce17 100644
--- a/Test/dafny0/NonGhostQuantifiers.dfy.expect
+++ b/Test/dafny0/NonGhostQuantifiers.dfy.expect
@@ -18,4 +18,4 @@ NonGhostQuantifiers.dfy(106,5): Error: quantifiers in non-ghost contexts must be
 NonGhostQuantifiers.dfy(114,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'

 NonGhostQuantifiers.dfy(123,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'

 NonGhostQuantifiers.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-20 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\NonGhostQuantifiers.dfy

+20 resolution/type errors detected in NonGhostQuantifiers.dfy

diff --git a/Test/dafny0/ParallelResolveErrors.dfy.expect b/Test/dafny0/ParallelResolveErrors.dfy.expect
index 171e66e1..78a43ed9 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy.expect
+++ b/Test/dafny0/ParallelResolveErrors.dfy.expect
@@ -19,4 +19,4 @@ ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scop
 ParallelResolveErrors.dfy(107,9): Error: the body of the enclosing forall statement is not allowed to update heap locations

 ParallelResolveErrors.dfy(115,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

 ParallelResolveErrors.dfy(120,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

-21 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\ParallelResolveErrors.dfy

+21 resolution/type errors detected in ParallelResolveErrors.dfy

diff --git a/Test/dafny0/ParseErrors.dfy.expect b/Test/dafny0/ParseErrors.dfy.expect
index ed018bea..e1acb035 100644
--- a/Test/dafny0/ParseErrors.dfy.expect
+++ b/Test/dafny0/ParseErrors.dfy.expect
@@ -12,4 +12,4 @@ ParseErrors.dfy(66,2): error: this operator cannot continue this calculation
 ParseErrors.dfy(71,2): error: this operator cannot continue this calculation

 ParseErrors.dfy(72,2): error: this operator cannot continue this calculation

 ParseErrors.dfy(78,2): error: this operator cannot continue this calculation

-14 parse errors detected in c:\codeplex\dafny\Test\dafny0\ParseErrors.dfy

+14 parse errors detected in ParseErrors.dfy

diff --git a/Test/dafny0/RefinementErrors.dfy.expect b/Test/dafny0/RefinementErrors.dfy.expect
index 12183e32..40cdb081 100644
--- a/Test/dafny0/RefinementErrors.dfy.expect
+++ b/Test/dafny0/RefinementErrors.dfy.expect
@@ -9,4 +9,4 @@ RefinementErrors.dfy(38,13): Error: type parameters are not allowed to be rename
 RefinementErrors.dfy(39,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq<C>' instead of 'set<C>')

 RefinementErrors.dfy(40,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines

 RefinementErrors.dfy(57,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G

-11 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\RefinementErrors.dfy

+11 resolution/type errors detected in RefinementErrors.dfy

diff --git a/Test/dafny0/RefinementModificationChecking.dfy.expect b/Test/dafny0/RefinementModificationChecking.dfy.expect
index 997d1279..060ee3e4 100644
--- a/Test/dafny0/RefinementModificationChecking.dfy.expect
+++ b/Test/dafny0/RefinementModificationChecking.dfy.expect
@@ -1,3 +1,3 @@
 RefinementModificationChecking.dfy(19,4): Error: cannot assign to variable defined previously

 RefinementModificationChecking.dfy(20,4): Error: cannot assign to variable defined previously

-2 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\RefinementModificationChecking.dfy

+2 resolution/type errors detected in RefinementModificationChecking.dfy

diff --git a/Test/dafny0/ReturnErrors.dfy.expect b/Test/dafny0/ReturnErrors.dfy.expect
index 2d57c731..a2b9d86d 100644
--- a/Test/dafny0/ReturnErrors.dfy.expect
+++ b/Test/dafny0/ReturnErrors.dfy.expect
@@ -1,4 +1,4 @@
 ReturnErrors.dfy(32,10): Error: cannot have method call in return statement.

 ReturnErrors.dfy(38,10): Error: cannot have effectful parameter in multi-return statement.

 ReturnErrors.dfy(43,10): Error: can only have initialization methods which modify at most 'this'.

-3 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\ReturnErrors.dfy

+3 resolution/type errors detected in ReturnErrors.dfy

diff --git a/Test/dafny0/Simple.dfy.expect b/Test/dafny0/Simple.dfy.expect
index c187ffe1..aceb685a 100644
--- a/Test/dafny0/Simple.dfy.expect
+++ b/Test/dafny0/Simple.dfy.expect
@@ -1,4 +1,4 @@
-// c:\codeplex\dafny\Test\dafny0\Simple.dfy

+// Simple.dfy

 

 class MyClass<T, U> {

   var x: int;

diff --git a/Test/dafny0/TailCalls.dfy.expect b/Test/dafny0/TailCalls.dfy.expect
index ac9e803b..7fc51902 100644
--- a/Test/dafny0/TailCalls.dfy.expect
+++ b/Test/dafny0/TailCalls.dfy.expect
@@ -3,4 +3,4 @@ TailCalls.dfy(33,12): Error: 'decreases *' is allowed only on tail-recursive met
 TailCalls.dfy(40,12): Error: 'decreases *' is allowed only on tail-recursive methods

 TailCalls.dfy(45,12): Error: 'decreases *' is allowed only on tail-recursive methods

 TailCalls.dfy(67,12): Error: 'decreases *' is allowed only on tail-recursive methods

-5 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\TailCalls.dfy

+5 resolution/type errors detected in TailCalls.dfy

diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect
index 79faccae..62e41019 100644
--- a/Test/dafny0/TypeTests.dfy.expect
+++ b/Test/dafny0/TypeTests.dfy.expect
@@ -31,4 +31,4 @@ TypeTests.dfy(128,15): Error: ghost variables are allowed only in specification
 TypeTests.dfy(138,4): Error: cannot assign to non-ghost variable in a ghost context

 TypeTests.dfy(139,7): Error: cannot assign to non-ghost variable in a ghost context

 TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

-33 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\TypeTests.dfy

+33 resolution/type errors detected in TypeTests.dfy