diff options
| author |  qunyanm <unknown> | 2015-03-27 16:54:42 -0700 |
|---|---|---|
| committer | qunyanm <unknown> | 2015-03-27 16:54:42 -0700 |
| commit | 441eca2a4c02efcc555cb8ca25ac991ccee205f8 (patch) | |
| tree | 5409284ced3580ed351d63f606929ef799597182 /Test/dafny4 | |
| parent | 3b5da042259432b62b70300e48f12cbdffdcf796 (diff) | |
Fix issue #56. Convert parametered opaque type parameters into an IdentifierExpr
instead of FunctionCall.
Diffstat (limited to 'Test/dafny4')
| -rw-r--r-- | Test/dafny4/Bug56.dfy | 23 | ||||
| -rw-r--r-- | Test/dafny4/Bug56.dfy.expect | 2 |
2 files changed, 25 insertions, 0 deletions
diff --git a/Test/dafny4/Bug56.dfy b/Test/dafny4/Bug56.dfy new file mode 100644 index 00000000..3d3839ed --- /dev/null +++ b/Test/dafny4/Bug56.dfy @@ -0,0 +1,23 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function I(f:int->bool):int->bool
+ ensures I(f) == f;
+
+predicate G<S>(s:S)
+
+type D<X>
+type E
+
+lemma L1<S>(b:int->S)
+ requires forall i :: b.reads(i) == {};
+ requires forall i :: b.requires(i);
+ requires I(j => G(b(j)))(0); // PRECONDITION NOT SATISFIED BY L2
+
+lemma L2(b:int->D<E>)
+ requires forall i :: b.reads(i) == {};
+ requires forall i :: b.requires(i);
+ requires I(j => G(b(j)))(0);
+{
+ L1(b); // FAILS TO SATISFY L1's PRECONDITION
+}
\ No newline at end of file diff --git a/Test/dafny4/Bug56.dfy.expect b/Test/dafny4/Bug56.dfy.expect new file mode 100644 index 00000000..790f6509 --- /dev/null +++ b/Test/dafny4/Bug56.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 5 verified, 0 errors
|