diff options
-rw-r--r-- | Dafny/DafnyAst.cs | 13 | ||||
-rw-r--r-- | Dafny/RefinementTransformer.cs | 7 | ||||
-rw-r--r-- | Dafny/Translator.cs | 10 | ||||
-rw-r--r-- | Test/dafny0/Answer | 18 | ||||
-rw-r--r-- | Test/dafny0/Refinement.dfy | 24 |
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 + } + } +} |