diff options
author | Rustan Leino <unknown> | 2013-04-01 14:28:37 -0700 |
---|---|---|
committer | Rustan Leino <unknown> | 2013-04-01 14:28:37 -0700 |
commit | 7ee036cae0cc6a2d48786f18908f26de37136236 (patch) | |
tree | d8e3965854d7499f754551695f694cee8a7acbe5 /Test/dafny0/ResolutionErrors.dfy | |
parent | 5152d9cd2fd4cd7258d745ec01324b4b654e1172 (diff) |
Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, where more type information is known
Refactored ConcreteUpdateStatement to no longer inherit from ConcreteSyntaxStatement.
Fixed numerous places where some recursive checks did not reach.
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy')
-rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 696a583f..60314836 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -626,3 +626,19 @@ module GhostAllocationTests { {
}
}
+
+// ------------------------- underspecified types ------------------------------
+
+module UnderspecifiedTypes {
+ method M(S: set<int>) {
+ var n, p, T0 :| 12 <= n && n in T0 && 10 <= p && p in T0 && T0 <= S && p % 2 != n % 2;
+ var T1 :| 12 in T1 && T1 <= S;
+ var T2 :| T2 <= S && 12 in T2;
+ var T3 :| 120 in T3; // error: underspecified type
+ var T3'0: set<int> :| 120 in T3'0;
+ var T3'1: multiset<int> :| 120 in T3'1;
+ var T3'2: map<int,bool> :| 120 in T3'2;
+ var T3'3: seq<int> :| 120 in T3'3;
+ var T4 :| T4 <= S;
+ }
+}
|