Members included from different files are now internally marked with an IncludeToken; the previous scheme of using {:verify false} is no longer used. This makes "include" work with refinement features.

Filenames of included files used in error messages are now what the user wrote, rather than absolute paths (which not only don't look so good, but are also problematic in comparing test output on different machines).
Added dafny0/Includee.dfy to the test suite as well -- might as well include it, too, to get checked.

9 files changed, 123 insertions, 70 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 8d4ddb8f..b54e3a6b 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -191,11 +191,13 @@ Dafny
   { "include" string                            (. {

                                                     string parsedFile = t.filename;

                                                     string includedFile = t.val.Substring(1, t.val.Length - 2);

+                                                    string fullPath = includedFile;

                                                     if (!Path.IsPathRooted(includedFile)) {

                                                       string basePath = Path.GetDirectoryName(parsedFile);

-                                                      includedFile = Path.GetFullPath(Path.Combine(basePath, includedFile));

-                                                    } 

-                                                    defaultModule.Includes.Add(new Include(t, includedFile)); 

+                                                      includedFile = Path.Combine(basePath, includedFile);

+                                                      fullPath = Path.GetFullPath(includedFile);

+                                                    }

+                                                    defaultModule.Includes.Add(new Include(t, includedFile, fullPath)); 

                                                    }

                                                 .) 

   }

@@ -617,16 +619,6 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
   [ BlockStmt<out body, out bodyStart, out bodyEnd>

   ]

   (. 

-     if (!theVerifyThisFile) {

-       body = null;

-       

-        List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

-        Attributes.Argument/*!*/ anArg;

-        anArg = new Attributes.Argument(id, new LiteralExpr(t, false));

-        args.Add(anArg);

-        attrs = new Attributes("verify", args, attrs);

-     }

-

      if (Attributes.Contains(attrs, "axiom") && !mmod.IsGhost && !isLemma) {

         SemErr(t, "only ghost methods can have the :axiom attribute");

      }

@@ -635,17 +627,18 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
         SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");

      }

 

+     IToken tok = theVerifyThisFile ? id : new IncludeToken(id);

      if (isConstructor) {

-       m = new Constructor(id, hasName ? id.val : "_ctor", typeArgs, ins,

+       m = new Constructor(tok, hasName ? id.val : "_ctor", typeArgs, ins,

                            req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

      } else if (isCoLemma) {

-       m = new CoLemma(id, id.val, mmod.IsStatic, typeArgs, ins, outs,

+       m = new CoLemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs,

                        req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

      } else if (isLemma) {

-       m = new Lemma(id, id.val, mmod.IsStatic, typeArgs, ins, outs,

+       m = new Lemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs,

                      req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

      } else {

-       m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs,

+       m = new Method(tok, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs,

                       req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

      }

      m.BodyStartTok = bodyStart;

@@ -884,26 +877,19 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
   { FunctionSpec<reqs, reads, ens, decreases> }

   [ FunctionBody<out body, out bodyStart, out bodyEnd>

   ]

-  (. if (!theVerifyThisFile) {  // We still need the func bodies, but don't bother verifying their correctness

-        List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

-        Attributes.Argument/*!*/ anArg;

-        anArg = new Attributes.Argument(id, new LiteralExpr(t, false));

-        args.Add(anArg);

-        attrs = new Attributes("verify", args, attrs);

-     } 

-

-     if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom")) {

+  (. if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom")) {

         SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute");

      }

 

+     IToken tok = theVerifyThisFile ? id : new IncludeToken(id);

      if (isPredicate) {

-        f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

+        f = new Predicate(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

                           reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureEllipsis);

      } else if (isCoPredicate) {

-        f = new CoPredicate(id, id.val, mmod.IsStatic, typeArgs, openParen, formals,

+        f = new CoPredicate(tok, id.val, mmod.IsStatic, typeArgs, openParen, formals,

                           reqs, reads, ens, body, attrs, signatureEllipsis);

      } else {

-        f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,

+        f = new Function(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,

                          reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureEllipsis);

      }

      f.BodyStartTok = bodyStart;

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index db528ceb..7b88d0bb 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -49,17 +49,20 @@ namespace Microsoft.Dafny {
   public class Include : IComparable

   {

     public readonly IToken tok;

-    public readonly string filename;    

+    public readonly string filename;

+    public readonly string fullPath;

 

-    public Include(IToken tok, string theFilename) {

+    public Include(IToken tok, string theFilename, string fullPath) {

       this.tok = tok;

-      this.filename = theFilename;      

+      this.filename = theFilename;

+      this.fullPath = fullPath;

     }

 

 

     public int CompareTo(object obj) {

-      if (obj is Include) {

-        return this.filename.CompareTo(((Include)obj).filename);

+      var i = obj as Include;

+      if (i != null) {

+        return this.fullPath.CompareTo(i.fullPath);

       } else {

         throw new NotImplementedException();

       }

@@ -3964,6 +3967,19 @@ namespace Microsoft.Dafny {
     public readonly IToken Inner;

   }

 

+  /// <summary>

+  /// An IncludeToken is a wrapper that indicates that the function/method was

+  /// declared in a file that was included. Any proof obligations from such an

+  /// included file are to be ignored.

+  /// </summary>

+  public class IncludeToken : TokenWrapper

+  {

+    public IncludeToken(IToken wrappedToken)

+      : base(wrappedToken) {

+      Contract.Requires(wrappedToken != null);

+    }

+  }

+

   // ------------------------------------------------------------------------------------------------------

 

   public abstract class Expression

diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
index b608a6e2..f604ebe6 100644
--- a/Source/Dafny/DafnyMain.cs
+++ b/Source/Dafny/DafnyMain.cs
@@ -86,13 +86,13 @@ namespace Microsoft.Dafny {
     // Lower-case file names before comparing them, since Windows uses case-insensitive file names

     private class IncludeComparer : IComparer<Include> {

       public int Compare(Include x, Include y) {

-        return x.filename.ToLower().CompareTo(y.filename.ToLower());

+        return x.fullPath.ToLower().CompareTo(y.fullPath.ToLower());

       }

     }

 

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

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

-      bool newlyIncluded = false;

+      bool newlyIncluded;

       do {

         newlyIncluded = false;

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index ce73beb4..1b30b886 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -242,11 +242,13 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
 			{

 			string parsedFile = t.filename;

 			string includedFile = t.val.Substring(1, t.val.Length - 2);

+			string fullPath = includedFile;

 			if (!Path.IsPathRooted(includedFile)) {

 			  string basePath = Path.GetDirectoryName(parsedFile);

-			  includedFile = Path.GetFullPath(Path.Combine(basePath, includedFile));

-			} 

-			defaultModule.Includes.Add(new Include(t, includedFile)); 

+			  includedFile = Path.Combine(basePath, includedFile);

+			  fullPath = Path.GetFullPath(includedFile);

+			}

+			defaultModule.Includes.Add(new Include(t, includedFile, fullPath)); 

 			}

 			

 		}

@@ -815,26 +817,19 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
 		if (la.kind == 9) {

 			FunctionBody(out body, out bodyStart, out bodyEnd);

 		}

-		if (!theVerifyThisFile) {  // We still need the func bodies, but don't bother verifying their correctness

-		  List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

-		  Attributes.Argument/*!*/ anArg;

-		  anArg = new Attributes.Argument(id, new LiteralExpr(t, false));

-		  args.Add(anArg);

-		  attrs = new Attributes("verify", args, attrs);

-		} 

-		

 		if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom")) {

 		  SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute");

 		}

 		

+		IToken tok = theVerifyThisFile ? id : new IncludeToken(id);

 		if (isPredicate) {

-		  f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

+		  f = new Predicate(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

 		                    reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureEllipsis);

 		} else if (isCoPredicate) {

-		  f = new CoPredicate(id, id.val, mmod.IsStatic, typeArgs, openParen, formals,

+		  f = new CoPredicate(tok, id.val, mmod.IsStatic, typeArgs, openParen, formals,

 		                    reqs, reads, ens, body, attrs, signatureEllipsis);

 		} else {

-		  f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,

+		  f = new Function(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,

 		                   reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureEllipsis);

 		}

 		f.BodyStartTok = bodyStart;

@@ -940,16 +935,6 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
 		if (la.kind == 9) {

 			BlockStmt(out body, out bodyStart, out bodyEnd);

 		}

-		if (!theVerifyThisFile) {

-		 body = null;

-		 

-		  List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

-		  Attributes.Argument/*!*/ anArg;

-		  anArg = new Attributes.Argument(id, new LiteralExpr(t, false));

-		  args.Add(anArg);

-		  attrs = new Attributes("verify", args, attrs);

-		}

-		

 		if (Attributes.Contains(attrs, "axiom") && !mmod.IsGhost && !isLemma) {

 		  SemErr(t, "only ghost methods can have the :axiom attribute");

 		}

@@ -958,17 +943,18 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
 		  SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");

 		}

 		

+		IToken tok = theVerifyThisFile ? id : new IncludeToken(id);

 		if (isConstructor) {

-		 m = new Constructor(id, hasName ? id.val : "_ctor", typeArgs, ins,

+		 m = new Constructor(tok, hasName ? id.val : "_ctor", typeArgs, ins,

 		                     req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

 		} else if (isCoLemma) {

-		 m = new CoLemma(id, id.val, mmod.IsStatic, typeArgs, ins, outs,

+		 m = new CoLemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs,

 		                 req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

 		} else if (isLemma) {

-		 m = new Lemma(id, id.val, mmod.IsStatic, typeArgs, ins, outs,

+		 m = new Lemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs,

 		               req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

 		} else {

-		 m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs,

+		 m = new Method(tok, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs,

 		                req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

 		}

 		m.BodyStartTok = bodyStart;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 85b6d214..b622b792 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1086,7 +1086,7 @@ namespace Microsoft.Dafny {
         } else if (member is Function) {

           var f = (Function)member;

           AddClassMember_Function(f);

-          if (!IsOpaqueFunction(f) && !f.IsBuiltin) { // Opaque function's well-formedness is checked on the full version

+          if (!IsOpaqueFunction(f) && !f.IsBuiltin && !(f.tok is IncludeToken)) { // Opaque function's well-formedness is checked on the full version

             AddWellformednessCheck(f);

           }

           var cop = f as CoPredicate;

@@ -1104,7 +1104,9 @@ namespace Microsoft.Dafny {
           } else {

             var proc = AddMethod(m, MethodTranslationKind.SpecWellformedness);

             sink.TopLevelDeclarations.Add(proc);

-            AddMethodImpl(m, proc, true);

+            if (!(m.tok is IncludeToken)) {

+              AddMethodImpl(m, proc, true);

+            }

           }

           // the method spec itself

           sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.InterModuleCall));

@@ -1115,7 +1117,7 @@ namespace Microsoft.Dafny {
             m = ((CoLemma)m).PrefixLemma;

             sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.CoCall));

           }

-          if (m.Body != null) {

+          if (m.Body != null && !(m.tok is IncludeToken)) {

             // ...and its implementation

             var proc = AddMethod(m, MethodTranslationKind.Implementation);

             sink.TopLevelDeclarations.Add(proc);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 7f197969..57c0b11e 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2112,8 +2112,36 @@ Execution trace:
 Dafny program verifier finished with 7 verified, 5 errors

 

 -------------------- Include.dfy --------------------

+Include.dfy(17,19): Error BP5003: A postcondition might not hold on this return path.

+Includee.dfy(15,20): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+Includee.dfy[Concrete](20,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Include.dfy(25,7): Error BP5003: A postcondition might not hold on this return path.

+Includee.dfy[Concrete](18,15): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Then

 

-Dafny program verifier finished with 2 verified, 0 errors

+Dafny program verifier finished with 4 verified, 3 errors

+

+-------------------- Includee.dfy --------------------

+Includee.dfy(19,3): Error BP5003: A postcondition might not hold on this return path.

+Includee.dfy(18,15): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+Includee.dfy(22,18): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Includee.dfy(4,1): Error BP5003: A postcondition might not hold on this return path.

+Includee.dfy(3,13): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 5 verified, 3 errors

 

 -------------------- AutoReq.dfy --------------------

 AutoReq.dfy(245,3): Error: possible violation of function precondition

diff --git a/Test/dafny0/Include.dfy b/Test/dafny0/Include.dfy
index a228194f..00458dc3 100644
--- a/Test/dafny0/Include.dfy
+++ b/Test/dafny0/Include.dfy
@@ -10,3 +10,22 @@ method test_include(z:int)
   var w := m_unproven(z);

   assert w == 2*z;

 }

+

+// and some refinement stuff, to make sure it works with includes

+module Concrete refines Abstract

+{

+  function method inc...  // error: postcondition violation

+  {

+    x - 1

+  }

+  method M...

+  {

+    var y := G(x);  // error: it is not know whether or not G(x) is non-negative, as required

+    if x < 68 {

+      return 70;  // error

+    } else if 30 <= x {  // this will always be true here

+      return x;  // fine

+    }

+    ...;

+  }

+}

diff --git a/Test/dafny0/Includee.dfy b/Test/dafny0/Includee.dfy
index 303e8dd4..6d2e17e0 100644
--- a/Test/dafny0/Includee.dfy
+++ b/Test/dafny0/Includee.dfy
@@ -1,10 +1,26 @@
 

 method m_unproven(x:int) returns (y:int)

   ensures y == 2*x;

-{

+{  // error: postcondition violation

 }

 

 function f(x:int) : int

 {

   2*x

 }

+

+abstract module Abstract

+{

+  function method inc(x:int) :int

+    ensures inc(x) > x;

+

+  method M(x: int) returns (r: int)

+    ensures r == x;

+  {  // error: postcondition violation

+    var y :| 0 <= y;

+    r := x + 3;

+    assert r % 3 == 0;  // error

+  }

+

+  function method G(x: int): int

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index faa08a29..38e37d5d 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -29,7 +29,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy RealTypes.dfy Definedness.dfy
             IteratorResolution.dfy Iterators.dfy

             RankPos.dfy RankNeg.dfy

             Computations.dfy ComputationsNeg.dfy

-            Include.dfy AutoReq.dfy DatatypeUpdate.dfy ModifyStmt.dfy SeqSlice.dfy

+            Include.dfy Includee.dfy AutoReq.dfy DatatypeUpdate.dfy ModifyStmt.dfy SeqSlice.dfy

             RealCompare.dfy) do (

   echo.

   echo -------------------- %%f --------------------