Dafny: make sure assume->assert transformation gives rise to a check

5 files changed, 67 insertions, 5 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 27fbb05c..c9c0ec08 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -101,7 +101,18 @@ namespace Microsoft.Dafny {
       Prev = prev;

     }

 

-    public class Argument {

+    public static bool Contains(Attributes attrs, string nm) {

+      Contract.Requires(nm != null);

+      for (; attrs != null; attrs = attrs.Prev) {

+        if (attrs.Name == nm) {

+          return true;

+        }

+      }

+      return false;

+    }

+

+    public class Argument

+    {

       public readonly IToken Tok;

       public readonly string S;

       public readonly Expression E;

diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index df31a834..1626cdb4 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -797,7 +797,12 @@ namespace Microsoft.Dafny {
               if (oldAssume == null) {

                 reporter.Error(cur.Tok, "assert template does not match old statement");

               } else {

-                body.Add(new AssertStmt(ass.Tok, CloneExpr(oldAssume.Expr)));

+                // Clone the expression, but among the new assert's attributes, indicate

+                // that this assertion is supposed to be translated into a check.  That is,

+                // it is not allowed to be just assumed in the translation, despite the fact

+                // that the condition is inherited.

+                var e = CloneExpr(oldAssume.Expr);

+                body.Add(new AssertStmt(ass.Tok, e, new Attributes("prependAssertToken", new List<Attributes.Argument>(), null)));

               }

               i++; j++;

             } else {

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 8135a61a..c0a56d05 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -3276,14 +3276,20 @@ namespace Microsoft.Dafny {
           AddComment(builder, stmt, "assert statement");

           PredicateStmt s = (PredicateStmt)stmt;

           TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);

+          IToken enclosingToken = null;

+          if (Attributes.Contains(stmt.Attributes, "prependAssertToken")) {

+            enclosingToken = stmt.Tok;

+          }

           bool splitHappened;

           var ss = TrSplitExpr(s.Expr, etran, out splitHappened);

           if (!splitHappened) {

-            builder.Add(Assert(s.Expr.tok, etran.TrExpr(s.Expr), "assertion violation"));

+            var tok = enclosingToken == null ? s.Expr.tok : new NestedToken(enclosingToken, s.Expr.tok);

+            builder.Add(Assert(tok, etran.TrExpr(s.Expr), "assertion violation"));

           } else {

             foreach (var split in ss) {

               if (!split.IsFree) {

-                builder.Add(AssertNS(split.E.tok, split.E, "assertion violation"));

+                var tok = enclosingToken == null ? split.E.tok : new NestedToken(enclosingToken, split.E.tok);

+                builder.Add(AssertNS(tok, split.E, "assertion violation"));

               }

             }

             builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 8cb67403..d0dfc9be 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1359,8 +1359,24 @@ Refinement.dfy(93,3): Error BP5003: A postcondition might not hold on this retur
 Refinement.dfy(74,15): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

+Refinement.dfy(179,5): Error BP5003: A postcondition might not hold on this return path.

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

+Refinement.dfy(176,9): Related location: Related location

+Execution trace:

+    (0,0): anon0

+Refinement.dfy(183,5): Error BP5003: A postcondition might not hold on this return path.

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

+Refinement.dfy(176,9): Related location: Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Then

+    (0,0): anon3

+Refinement.dfy(189,7): Error: assertion violation

+Refinement.dfy[IncorrectConcrete](128,24): Related location: Related location

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 44 verified, 6 errors

+Dafny program verifier finished with 48 verified, 9 errors

 

 -------------------- RefinementErrors.dfy --------------------

 RefinementErrors.dfy(27,17): Error: a refining method is not allowed to add preconditions

diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index c24ed555..da7f0ac2 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -166,3 +166,27 @@ module Client imports Concrete {
     }
   }
 }
+
+module IncorrectConcrete refines Abstract {
+  class MyNumber {
+    var a: int;
+    var b: int;
+    predicate Valid
+    {
+      N == 2*a - b
+    }
+    constructor Init()
+    {  // error: postcondition violation
+      a := b;
+    }
+    method Inc()
+    {  // error: postcondition violation
+      if (*) { a := a + 1; } else { b := b - 1; }
+    }
+    method Get() returns (n: int)
+    {
+      var k := a - b;
+      assert ...;  // error: assertion violation
+    }
+  }
+}