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/RefinementTransformer.cs | |
| parent | 5b6de79e16850e70a9ab1a37ba45245275c3fd20 (diff) | |
Dafny: make sure assume->assert transformation gives rise to a check
Diffstat (limited to 'Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Dafny/RefinementTransformer.cs | 7 |
1 files changed, 6 insertions, 1 deletions
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 {
|