diff options
| author |  leino <unknown> | 2015-01-07 11:16:18 -0800 |
|---|---|---|
| committer | leino <unknown> | 2015-01-07 11:16:18 -0800 |
| commit | 2e68bc2f862a9230056b0a5db59228fbce2d78ab (patch) | |
| tree | a9eeda2fade5ec0ef46ff155c3adf7baf529b9ee /Test/dafny0/OpaqueFunctions.dfy | |
| parent | 57d62186efa929c0623a69453c8e4196ac9803a4 (diff) | |
Fixed bug in opaque functions with type parameters
Diffstat (limited to 'Test/dafny0/OpaqueFunctions.dfy')
| -rw-r--r-- | Test/dafny0/OpaqueFunctions.dfy | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy index d00e1246..64e63293 100644 --- a/Test/dafny0/OpaqueFunctions.dfy +++ b/Test/dafny0/OpaqueFunctions.dfy @@ -218,3 +218,24 @@ module LayerQuantifiers assert f(one + one + one);
}
}
+
+// ------------------------------------- regression test
+
+module Regression
+{
+ datatype List<A> = Nil | Cons(A, tl: List<A>)
+
+ function Empty<A>(): List<A> { Nil }
+
+ function {:opaque} Length<A>(s: List<A>): int
+ ensures 0 <= Length(s)
+ {
+ if s.Cons? then 1 + Length(s.tl) else 0
+ }
+
+ lemma Empty_ToZero<A>()
+ ensures Length<A>(Empty<A>()) == 0; // this line once caused the verifier to crash
+ {
+ reveal_Length();
+ }
+}
|