diff options
Diffstat (limited to 'Test')
-rw-r--r-- | Test/dafny0/Answer | 11 | ||||
-rw-r--r-- | Test/dafny0/TypeParameters.dfy | 22 |
2 files changed, 31 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 0c152d6e..cc248c20 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -389,8 +389,17 @@ Execution trace: TypeParameters.dfy(63,27): Error: assertion violation
Execution trace:
(0,0): anon0
+TypeParameters.dfy(130,28): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Then
+TypeParameters.dfy(132,33): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
+ (0,0): anon6_Then
-Dafny program verifier finished with 24 verified, 2 errors
+Dafny program verifier finished with 27 verified, 4 errors
-------------------- Datatypes.dfy --------------------
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index e199a386..61a0019b 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -103,7 +103,7 @@ static function IsCelebrity<Person>(c: Person, people: set<Person>): bool; requires c == c || c in people;
method FindCelebrity3(people: set<int>, ghost c: int)
- requires IsCelebrity(c, people);
+ requires IsCelebrity(c, people); // once upon a time, this caused the translator to produce bad Boogie
{
ghost var b: bool;
b := IsCelebrity(c, people);
@@ -112,3 +112,23 @@ method FindCelebrity3(people: set<int>, ghost c: int) static function F(c: int, people: set<int>): bool;
requires IsCelebrity(c, people);
+
+function RogerThat<G>(g: G): G
+{
+ g
+}
+
+function Cool(b: bool): bool
+{
+ b
+}
+
+method IsRogerCool(n: int)
+ requires RogerThat(true); // once upon a time, this caused the translator to produce bad Boogie
+{
+ if (*) {
+ assert Cool(2 < 3 && n < n && n < n+1); // the error message here will peek into the argument of Cool
+ } else if (*) {
+ assert RogerThat(2 < 3 && n < n && n < n+1); // same here; cool, huh?
+ }
+}
|