diff options
| author |  Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-14 23:51:17 +0200 |
|---|---|---|
| committer | Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-14 23:51:17 +0200 |
| commit | b13941f65117bb3d8741f26b0f9d76dc976fe419 (patch) | |
| tree | a63f244dcd819f82d306f8fb57f64e33d03e7af5 | |
| parent | 1b291079446ae1f74cd92705546c76f86496e22d (diff) | |
Error reporting for calculation steps
| -rw-r--r-- | Dafny/Translator.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index 31e39af2..b486681b 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -4012,7 +4012,7 @@ namespace Microsoft.Dafny { TrStmt(h, b, locals, etran);
}
// NadiaTodo: add error messages
- b.Add(new Bpl.AssertCmd(s.Tok, etran.TrExpr(s.Steps[i])));
+ b.Add(Assert(s.Terms[i + 1].tok, etran.TrExpr(s.Steps[i]), "this calculation step might not hold"));
b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
if (i == s.Steps.Count - 1) {
// first iteration (last step)
|