diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-02-19 00:18:00 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-02-19 00:18:00 -0800 |
| commit | ba75a2d0b67ce5c330abd1903a6942a9b385d361 (patch) | |
| tree | f77ac15c01adc43eb052f1b29dfa402eb7c87832 /Dafny | |
| parent | 5b6de79e16850e70a9ab1a37ba45245275c3fd20 (diff) | |
Dafny: make sure assume->assert transformation gives rise to a check
Diffstat (limited to 'Dafny')
| -rw-r--r-- | Dafny/DafnyAst.cs | 13 | ||||
| -rw-r--r-- | Dafny/RefinementTransformer.cs | 7 | ||||
| -rw-r--r-- | Dafny/Translator.cs | 10 |
3 files changed, 26 insertions, 4 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)));
|