diff options
| author |  Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-21 17:48:16 +0200 |
|---|---|---|
| committer | Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-21 17:48:16 +0200 |
| commit | 0f2e84ea7799c04f9b079398989fd503ae72aa52 (patch) | |
| tree | b2b3722410cedcc676a02b6c490887f33e37e5d9 /Test/dafny0/ResolutionErrors.dfy | |
| parent | 33d178877dbde9371dc77144f8c3881751ad8553 (diff) | |
Bugfix in the translation of calc statements (oops), added more resolution and verification tests
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index a7a84ebb..c615c5ec 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -376,5 +376,10 @@ method TestCalc(m: int, n: int, a: bool, b: bool) n + m;
n + m + 1;
==> n + m + 2; // error: ==> operator requires boolean lines
- }
+ }
+ calc {
+ n + m;
+ { print n + m; } // error: non-ghost statements are not allowed in hints
+ m + n;
+ }
}
|