diff options
author | qunyanm <unknown> | 2015-03-16 15:43:39 -0700 |
---|---|---|
committer | qunyanm <unknown> | 2015-03-16 15:43:39 -0700 |
commit | eb3c12b3f4151d55e244f14eaefc02aaaeadc7c8 (patch) | |
tree | 134c956746fed18f8e471acb31c4ace1d4f247b2 /Test/dafny4 | |
parent | afc332da8becf903fc1084fb37489938c81959bf (diff) |
Fix issue #55 and #64. When performing type argument substitution for function
F's corresponding F_FULL, make sure the function is indeed the FullVesion
before the substitution. Also keep the TypeArgsSubst for the enclosingClass in
the typeMap.
Diffstat (limited to 'Test/dafny4')
-rw-r--r-- | Test/dafny4/Bug55.dfy | 14 | ||||
-rw-r--r-- | Test/dafny4/Bug55.dfy.expect | 2 |
2 files changed, 16 insertions, 0 deletions
diff --git a/Test/dafny4/Bug55.dfy b/Test/dafny4/Bug55.dfy new file mode 100644 index 00000000..bcbef2e8 --- /dev/null +++ b/Test/dafny4/Bug55.dfy @@ -0,0 +1,14 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate {:opaque} G(f:int->bool)
+ reads f.reads;
+ requires f.requires(0);
+{
+ true
+}
+
+predicate A<T>(s:set<T>)
+
+predicate{:opaque} B(s:set<int>)
+ requires A(s);
diff --git a/Test/dafny4/Bug55.dfy.expect b/Test/dafny4/Bug55.dfy.expect new file mode 100644 index 00000000..790f6509 --- /dev/null +++ b/Test/dafny4/Bug55.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 5 verified, 0 errors
|