diff options
| author |  Jason Koenig <unknown> | 2012-07-11 16:18:30 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2012-07-11 16:18:30 -0700 |
| commit | 719bf67be5d917a8fe7889c8d131eb27533ca0ff (patch) | |
| tree | 2aa6e95c02b57a00dd33a45f09e9da8b3d2e89cc /Test | |
| parent | e2fa35ca7a769e483014ec03a7c91faf2196f678 (diff) | |
Dafny: fixed translation bug in maps with objects in the domain, added test case
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/Maps.dfy | 10 |
2 files changed, 11 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 6b7a1079..a0ddd7f1 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1585,7 +1585,7 @@ Maps.dfy(126,13): Error: assertion violation Execution trace:
(0,0): anon0
-Dafny program verifier finished with 30 verified, 2 errors
+Dafny program verifier finished with 32 verified, 2 errors
-------------------- LiberalEquality.dfy --------------------
LiberalEquality.dfy(18,14): Error: arguments must have the same type (got T and U)
diff --git a/Test/dafny0/Maps.dfy b/Test/dafny0/Maps.dfy index a49ac3c1..1c245952 100644 --- a/Test/dafny0/Maps.dfy +++ b/Test/dafny0/Maps.dfy @@ -180,3 +180,13 @@ method m14() assert u[1] == 1 && u[3] == 4;
assert domain(u) == {0, 1, 3, 4};
}
+
+class A { var x: int; }
+
+method m15(b: set<A>)
+ requires forall a | a in b :: a != null;
+{
+ var m := map a | a in b :: a.x;
+ var aa := new A;
+ assert aa !in m;
+}
\ No newline at end of file |