summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar leino <unknown>2015-09-20 22:08:57 -0700
committerGravatar leino <unknown>2015-09-20 22:08:57 -0700
commite1eb35cb37d49c30b5a24ed828dc1ea505b00cc2 (patch)
treea6f3a333042ff22395a7231d0c601c63264f8c7a /Test
parentf6fe9adfa18b3b6f4d0c2c92f3f91e06160c503c (diff)
Changes that only affect line numbers in test case
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny0/ResolutionErrors.dfy78
-rw-r--r--Test/dafny0/ResolutionErrors.dfy.expect326
2 files changed, 231 insertions, 173 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index d34fd8a5..d38d2506 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -195,7 +195,6 @@ class GhostTests {
decreases 112 - n;
{
label MyStructure: {
-//KRML(ghost) if (k % 17 == 0) { break MyStructure; } // error: break from ghost to non-ghost point
k := k + 1;
}
label MyOtherStructure:
@@ -218,7 +217,6 @@ class GhostTests {
case true => break LoopLabel1; // fine
}
} else if (m % 101 == 0) {
-//KRML(ghost) break break; // error: break out of non-ghost loop from ghost context
}
m := m + 3;
}
@@ -231,20 +229,73 @@ class GhostTests {
break break; // fine, since this is not a ghost context
} else if (*) {
break break break; // error: tries to break out of more loop levels than there are
+ }
+ q := q + 1;
+ }
+ } else if (n == t) {
+ }
+ n := n + 1;
+ p := p + 1;
+ }
+ }
+/***KRML method BreakMayNotBeFineHere_Ghost(ghost t: int)
+ {
+ var n := 0;
+ ghost var k := 0;
+ var p := 0;
+ while (true)
+ invariant n <= 112;
+ decreases 112 - n;
+ {
+ label MyStructure: {
+ if (k % 17 == 0) { break MyStructure; } // error: break from ghost to non-ghost point
+ k := k + 1;
+ }
+ label MyOtherStructure:
+ if (k % 17 == 0) {
+ break MyOtherStructure; // this break is fine
+ } else {
+ k := k + 1;
+ }
+
+ var dontKnow;
+ if (n == 112) {
+ ghost var m := 0;
+ label LoopLabel0:
+ label LoopLabel1:
+ while (m < 200) {
+ if (m % 103 == 0) {
+ if {
+ case true => break; // fine, since this breaks out of the enclosing ghost loop
+ case true => break LoopLabel0; // fine
+ case true => break LoopLabel1; // fine
+ }
+ } else if (m % 101 == 0) {
+ break break; // error: break out of non-ghost loop from ghost context
+ }
+ m := m + 3;
+ }
+ break;
+ } else if (dontKnow == 708) {
+ var q := 0;
+ while (q < 1) {
+ label IfNest:
+ if (p == 67) {
+ break break; // fine, since this is not a ghost context
} else if (*) {
-//KRML(ghost) break break; // fine, since this is not a ghost context
+ break break; // fine, since this is not a ghost context
} else if (k == 67) {
-//KRML(ghost) break break; // error, because this is a ghost context
+ break break; // error, because this is a ghost context
}
q := q + 1;
}
} else if (n == t) {
-//KRML(ghost) return; // error: this is a ghost context trying to return from a non-ghost method
+ return; // error: this is a ghost context trying to return from a non-ghost method
}
n := n + 1;
p := p + 1;
}
- }
+ }****/
}
method DuplicateLabels(n: int) {
@@ -310,9 +361,11 @@ method DatatypeDestructors(d: DTD_List) {
assert d.DTD_Cons? == d.Car; // type error
assert d == DTD_Cons(hd, tl, 5);
ghost var g0 := d.g; // fine
-//KRML(ghost) var g1 := d.g; // error: cannot use ghost member in non-ghost code
}
}
+method DatatypeDestructors_Ghost(d: DTD_List) {
+//KRML var g1 := d.g; // error: cannot use ghost member in non-ghost code
+}
// ------------------- print statements ---------------------------------------
@@ -381,9 +434,12 @@ method TestCalc(m: int, n: int, a: bool, b: bool)
n + m + 1;
==> n + m + 2; // error: ==> operator requires boolean lines
}
+}
+method TestCalc_Ghost(m: int, n: int, a: bool, b: bool)
+{
calc {
n + m;
-//KRML(ghost) { print n + m; } // error: non-ghost statements are not allowed in hints
+//KRML { print n + m; } // error: non-ghost statements are not allowed in hints
m + n;
}
}
@@ -543,12 +599,14 @@ method LetSuchThat(ghost z: int, n: nat)
var x: int;
x := var y :| y < 0; y; // fine for the resolver (but would give a verification error for not being deterministic)
-//KRML(ghost) x := var y :| y < z; y; // error: contraint depend on ghost (z)
-
x := var w :| w == 2*w; w; // fine (even for the verifier, this one)
x := var w := 2*w; w; // error: the 'w' in the RHS of the assignment is not in scope
ghost var xg := var w :| w == 2*w; w;
}
+method LetSuchThat_Ghost(ghost z: int, n: nat)
+{
+//KRML var x := var y :| y < z; y; // error: contraint depend on ghost (z)
+}
// ------------ quantified variables whose types are not inferred ----------
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 04913cf5..55d2e79c 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -1,112 +1,112 @@
-ResolutionErrors.dfy(502,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
-ResolutionErrors.dfy(507,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
-ResolutionErrors.dfy(521,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
-ResolutionErrors.dfy(533,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree
-ResolutionErrors.dfy(561,25): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(561,23): Error: type variable 'T' in the function call to 'P' could not be determined
-ResolutionErrors.dfy(568,25): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(568,23): Error: type variable 'T' in the function call to 'P' could not be determined
-ResolutionErrors.dfy(581,13): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(582,9): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(589,14): Error: new allocation not supported in forall statements
-ResolutionErrors.dfy(594,11): Error: the body of the enclosing forall statement is not allowed to update heap locations
-ResolutionErrors.dfy(594,14): Error: new allocation not allowed in ghost context
-ResolutionErrors.dfy(604,23): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(611,15): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(611,15): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(620,17): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(622,29): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(624,17): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(642,21): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(680,20): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(690,24): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(693,22): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(704,18): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(705,23): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(706,20): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(709,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(728,24): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(731,22): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(736,18): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(737,23): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(738,11): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(741,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(766,19): Error: calls to methods with side-effects are not allowed inside a statement expression
-ResolutionErrors.dfy(767,20): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(768,20): Error: wrong number of method result arguments (got 0, expected 1)
-ResolutionErrors.dfy(780,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(790,4): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(801,36): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(810,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(824,6): Error: RHS (of type B) not assignable to LHS (of type object)
-ResolutionErrors.dfy(825,6): Error: RHS (of type int) not assignable to LHS (of type object)
-ResolutionErrors.dfy(826,6): Error: RHS (of type B) not assignable to LHS (of type object)
-ResolutionErrors.dfy(831,6): Error: RHS (of type G) not assignable to LHS (of type object)
-ResolutionErrors.dfy(832,6): Error: RHS (of type Dt) not assignable to LHS (of type object)
-ResolutionErrors.dfy(833,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)
-ResolutionErrors.dfy(895,4): Error: LHS of array assignment must denote an array element (found seq<int>)
-ResolutionErrors.dfy(896,4): Error: LHS of array assignment must denote an array element (found seq<int>)
-ResolutionErrors.dfy(901,10): Error: LHS of assignment must denote a mutable field
-ResolutionErrors.dfy(902,10): Error: LHS of assignment must denote a mutable field
-ResolutionErrors.dfy(903,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(904,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(905,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(906,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(987,11): Error: Wrong number of type arguments (2 instead of 1) passed to array type: array3
-ResolutionErrors.dfy(988,11): Error: Wrong number of type arguments (2 instead of 1) passed to class: C
-ResolutionErrors.dfy(999,7): Error: Duplicate name of top-level declaration: BadSyn2
-ResolutionErrors.dfy(996,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List
-ResolutionErrors.dfy(997,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name or declare a module import 'opened?')
-ResolutionErrors.dfy(998,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
-ResolutionErrors.dfy(1005,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A
-ResolutionErrors.dfy(1008,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1012,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1021,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
-ResolutionErrors.dfy(1024,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1029,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1048,21): Error: unresolved identifier: x
-ResolutionErrors.dfy(1055,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
-ResolutionErrors.dfy(1067,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name or declare a module import 'opened?')
-ResolutionErrors.dfy(1077,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)
-ResolutionErrors.dfy(1082,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)
-ResolutionErrors.dfy(1087,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)
-ResolutionErrors.dfy(1088,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)
-ResolutionErrors.dfy(1093,13): Error: arguments must have the same type (got P<int> and P<X>)
-ResolutionErrors.dfy(1094,13): Error: arguments must have the same type (got P<bool> and P<X>)
-ResolutionErrors.dfy(1095,13): Error: arguments must have the same type (got P<int> and P<bool>)
-ResolutionErrors.dfy(1118,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
-ResolutionErrors.dfy(1120,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
-ResolutionErrors.dfy(1225,26): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1226,31): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1227,29): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1237,34): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1253,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
-ResolutionErrors.dfy(1254,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
-ResolutionErrors.dfy(1291,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
-ResolutionErrors.dfy(1301,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(1329,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)
-ResolutionErrors.dfy(1339,29): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(1341,49): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(1341,54): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(1362,11): Error: name of type (X) is used as a variable
-ResolutionErrors.dfy(1362,16): Error: name of type (X) is used as a variable
-ResolutionErrors.dfy(1363,11): Error: name of module (Y) is used as a variable
-ResolutionErrors.dfy(1363,16): Error: name of module (Y) is used as a variable
-ResolutionErrors.dfy(1364,11): Error: name of type (X) is used as a variable
-ResolutionErrors.dfy(1364,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #type, or a map with domain #type (instead got map<real, string>)
-ResolutionErrors.dfy(1365,11): Error: name of module (Y) is used as a variable
-ResolutionErrors.dfy(1365,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #module, or a map with domain #module (instead got map<real, string>)
-ResolutionErrors.dfy(1370,16): Error: name of type (X) is used as a variable
-ResolutionErrors.dfy(1370,13): Error: arguments must have the same type (got int and #type)
-ResolutionErrors.dfy(1371,16): Error: name of module (Y) is used as a variable
-ResolutionErrors.dfy(1371,13): Error: arguments must have the same type (got int and #module)
-ResolutionErrors.dfy(1372,4): Error: name of type (X) is used as a variable
-ResolutionErrors.dfy(1373,4): Error: name of module (Y) is used as a variable
-ResolutionErrors.dfy(1382,11): Error: type of RHS of assign-such-that statement must be boolean (got int)
-ResolutionErrors.dfy(1383,9): Error: type of RHS of assign-such-that statement must be boolean (got int)
-ResolutionErrors.dfy(1384,13): Error: type of RHS of assign-such-that statement must be boolean (got int)
-ResolutionErrors.dfy(1387,15): Error: type of RHS of let-such-that expression must be boolean (got int)
-ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor
+ResolutionErrors.dfy(558,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
+ResolutionErrors.dfy(563,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
+ResolutionErrors.dfy(577,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
+ResolutionErrors.dfy(589,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree
+ResolutionErrors.dfy(619,25): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(619,23): Error: type variable 'T' in the function call to 'P' could not be determined
+ResolutionErrors.dfy(626,25): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(626,23): Error: type variable 'T' in the function call to 'P' could not be determined
+ResolutionErrors.dfy(639,13): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(640,9): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(647,14): Error: new allocation not supported in forall statements
+ResolutionErrors.dfy(652,11): Error: the body of the enclosing forall statement is not allowed to update heap locations
+ResolutionErrors.dfy(652,14): Error: new allocation not allowed in ghost context
+ResolutionErrors.dfy(662,23): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(669,15): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(669,15): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(678,17): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(680,29): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(682,17): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(700,21): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(738,20): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(748,24): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(751,22): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(762,18): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(763,23): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(764,20): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(767,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(786,24): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(789,22): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(794,18): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(795,23): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(796,11): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(799,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(824,19): Error: calls to methods with side-effects are not allowed inside a statement expression
+ResolutionErrors.dfy(825,20): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(826,20): Error: wrong number of method result arguments (got 0, expected 1)
+ResolutionErrors.dfy(838,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(848,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(859,36): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(868,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(882,6): Error: RHS (of type B) not assignable to LHS (of type object)
+ResolutionErrors.dfy(883,6): Error: RHS (of type int) not assignable to LHS (of type object)
+ResolutionErrors.dfy(884,6): Error: RHS (of type B) not assignable to LHS (of type object)
+ResolutionErrors.dfy(889,6): Error: RHS (of type G) not assignable to LHS (of type object)
+ResolutionErrors.dfy(890,6): Error: RHS (of type Dt) not assignable to LHS (of type object)
+ResolutionErrors.dfy(891,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)
+ResolutionErrors.dfy(953,4): Error: LHS of array assignment must denote an array element (found seq<int>)
+ResolutionErrors.dfy(954,4): Error: LHS of array assignment must denote an array element (found seq<int>)
+ResolutionErrors.dfy(959,10): Error: LHS of assignment must denote a mutable field
+ResolutionErrors.dfy(960,10): Error: LHS of assignment must denote a mutable field
+ResolutionErrors.dfy(961,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(962,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(963,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(964,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(1045,11): Error: Wrong number of type arguments (2 instead of 1) passed to array type: array3
+ResolutionErrors.dfy(1046,11): Error: Wrong number of type arguments (2 instead of 1) passed to class: C
+ResolutionErrors.dfy(1057,7): Error: Duplicate name of top-level declaration: BadSyn2
+ResolutionErrors.dfy(1054,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List
+ResolutionErrors.dfy(1055,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name or declare a module import 'opened?')
+ResolutionErrors.dfy(1056,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
+ResolutionErrors.dfy(1063,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A
+ResolutionErrors.dfy(1066,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1070,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1079,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
+ResolutionErrors.dfy(1082,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1087,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1106,21): Error: unresolved identifier: x
+ResolutionErrors.dfy(1113,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
+ResolutionErrors.dfy(1125,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name or declare a module import 'opened?')
+ResolutionErrors.dfy(1135,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)
+ResolutionErrors.dfy(1140,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)
+ResolutionErrors.dfy(1145,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)
+ResolutionErrors.dfy(1146,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)
+ResolutionErrors.dfy(1151,13): Error: arguments must have the same type (got P<int> and P<X>)
+ResolutionErrors.dfy(1152,13): Error: arguments must have the same type (got P<bool> and P<X>)
+ResolutionErrors.dfy(1153,13): Error: arguments must have the same type (got P<int> and P<bool>)
+ResolutionErrors.dfy(1176,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
+ResolutionErrors.dfy(1178,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
+ResolutionErrors.dfy(1283,26): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1284,31): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1285,29): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1295,34): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1311,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
+ResolutionErrors.dfy(1312,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
+ResolutionErrors.dfy(1349,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
+ResolutionErrors.dfy(1359,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1387,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)
+ResolutionErrors.dfy(1397,29): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1399,49): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1399,54): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1420,11): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1420,16): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1421,11): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1421,16): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1422,11): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1422,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #type, or a map with domain #type (instead got map<real, string>)
+ResolutionErrors.dfy(1423,11): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1423,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #module, or a map with domain #module (instead got map<real, string>)
+ResolutionErrors.dfy(1428,16): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1428,13): Error: arguments must have the same type (got int and #type)
+ResolutionErrors.dfy(1429,16): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1429,13): Error: arguments must have the same type (got int and #module)
+ResolutionErrors.dfy(1430,4): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1431,4): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1440,11): Error: type of RHS of assign-such-that statement must be boolean (got int)
+ResolutionErrors.dfy(1441,9): Error: type of RHS of assign-such-that statement must be boolean (got int)
+ResolutionErrors.dfy(1442,13): Error: type of RHS of assign-such-that statement must be boolean (got int)
+ResolutionErrors.dfy(1445,15): Error: type of RHS of let-such-that expression must be boolean (got int)
+ResolutionErrors.dfy(488,2): Error: More than one anonymous constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
@@ -124,25 +124,25 @@ ResolutionErrors.dfy(141,21): Error: ghost variables are allowed only in specifi
ResolutionErrors.dfy(142,35): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(151,10): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(157,16): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(233,12): Error: trying to break out of more loop levels than there are enclosing loops
-ResolutionErrors.dfy(408,11): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(410,14): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(412,10): Error: a hint is not allowed to update a variable declared outside the hint
-ResolutionErrors.dfy(438,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
-ResolutionErrors.dfy(443,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
-ResolutionErrors.dfy(444,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
-ResolutionErrors.dfy(446,9): Error: class Lamb does not have an anonymous constructor
-ResolutionErrors.dfy(844,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
-ResolutionErrors.dfy(848,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(851,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(859,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(869,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(880,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(1036,23): Error: unresolved identifier: x
-ResolutionErrors.dfy(1039,20): Error: unresolved identifier: x
-ResolutionErrors.dfy(1042,23): Error: unresolved identifier: x
-ResolutionErrors.dfy(1044,19): Error: unresolved identifier: x
-ResolutionErrors.dfy(1046,19): Error: unresolved identifier: x
+ResolutionErrors.dfy(231,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(464,11): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(466,14): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(468,10): Error: a hint is not allowed to update a variable declared outside the hint
+ResolutionErrors.dfy(494,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
+ResolutionErrors.dfy(499,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
+ResolutionErrors.dfy(500,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
+ResolutionErrors.dfy(502,9): Error: class Lamb does not have an anonymous constructor
+ResolutionErrors.dfy(902,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
+ResolutionErrors.dfy(906,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(909,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(917,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(927,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(938,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1094,23): Error: unresolved identifier: x
+ResolutionErrors.dfy(1097,20): Error: unresolved identifier: x
+ResolutionErrors.dfy(1100,23): Error: unresolved identifier: x
+ResolutionErrors.dfy(1102,19): Error: unresolved identifier: x
+ResolutionErrors.dfy(1104,19): Error: unresolved identifier: x
ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3<T>)
@@ -156,39 +156,39 @@ ResolutionErrors.dfy(62,14): Error: accessing member 'M' requires an instance ex
ResolutionErrors.dfy(63,7): Error: unresolved identifier: N
ResolutionErrors.dfy(66,8): Error: non-function expression (of type int) is called with parameters
ResolutionErrors.dfy(67,14): Error: member 'z' does not exist in type 'Global'
-ResolutionErrors.dfy(260,4): Error: label shadows an enclosing label
-ResolutionErrors.dfy(265,2): Error: duplicate label
-ResolutionErrors.dfy(291,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(292,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(294,9): Error: a constructor is allowed to be called only when an object is being allocated
-ResolutionErrors.dfy(308,16): Error: arguments must have the same type (got int and DTD_List)
-ResolutionErrors.dfy(309,16): Error: arguments must have the same type (got DTD_List and int)
-ResolutionErrors.dfy(310,25): Error: arguments must have the same type (got bool and int)
-ResolutionErrors.dfy(322,15): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(347,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
-ResolutionErrors.dfy(359,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
-ResolutionErrors.dfy(367,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
-ResolutionErrors.dfy(372,6): Error: all lines in a calculation must have the same type (got int after bool)
-ResolutionErrors.dfy(375,6): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(375,6): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(376,10): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(376,10): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(381,10): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(381,10): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(470,7): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(476,2): Error: non-ghost variable cannot be assigned a value that depends on a ghost
-ResolutionErrors.dfy(549,18): Error: unresolved identifier: w
-ResolutionErrors.dfy(656,11): Error: lemmas are not allowed to have modifies clauses
-ResolutionErrors.dfy(918,9): Error: unresolved identifier: s
-ResolutionErrors.dfy(929,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
-ResolutionErrors.dfy(930,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
-ResolutionErrors.dfy(936,16): Error: condition is expected to be of type bool, but is int
-ResolutionErrors.dfy(937,16): Error: member 3 does not exist in datatype _tuple#3
-ResolutionErrors.dfy(937,26): Error: member x does not exist in datatype _tuple#2
-ResolutionErrors.dfy(960,15): Error: arguments to / must have the same type (got real and int)
-ResolutionErrors.dfy(961,10): Error: second argument to % must be of type int (instead got real)
-ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait
-ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)
-ResolutionErrors.dfy(1134,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
-ResolutionErrors.dfy(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors.dfy(311,4): Error: label shadows an enclosing label
+ResolutionErrors.dfy(316,2): Error: duplicate label
+ResolutionErrors.dfy(342,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(343,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(345,9): Error: a constructor is allowed to be called only when an object is being allocated
+ResolutionErrors.dfy(359,16): Error: arguments must have the same type (got int and DTD_List)
+ResolutionErrors.dfy(360,16): Error: arguments must have the same type (got DTD_List and int)
+ResolutionErrors.dfy(361,25): Error: arguments must have the same type (got bool and int)
+ResolutionErrors.dfy(375,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(400,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
+ResolutionErrors.dfy(412,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
+ResolutionErrors.dfy(420,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
+ResolutionErrors.dfy(425,6): Error: all lines in a calculation must have the same type (got int after bool)
+ResolutionErrors.dfy(428,6): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(428,6): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(429,10): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(429,10): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(434,10): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(434,10): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(526,7): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(532,2): Error: non-ghost variable cannot be assigned a value that depends on a ghost
+ResolutionErrors.dfy(603,18): Error: unresolved identifier: w
+ResolutionErrors.dfy(714,11): Error: lemmas are not allowed to have modifies clauses
+ResolutionErrors.dfy(976,9): Error: unresolved identifier: s
+ResolutionErrors.dfy(987,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
+ResolutionErrors.dfy(988,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
+ResolutionErrors.dfy(994,16): Error: condition is expected to be of type bool, but is int
+ResolutionErrors.dfy(995,16): Error: member 3 does not exist in datatype _tuple#3
+ResolutionErrors.dfy(995,26): Error: member x does not exist in datatype _tuple#2
+ResolutionErrors.dfy(1018,15): Error: arguments to / must have the same type (got real and int)
+ResolutionErrors.dfy(1019,10): Error: second argument to % must be of type int (instead got real)
+ResolutionErrors.dfy(1164,8): Error: new cannot be applied to a trait
+ResolutionErrors.dfy(1185,13): Error: first argument to / must be of numeric type (instead got set<bool>)
+ResolutionErrors.dfy(1192,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors.dfy(1207,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
193 resolution/type errors detected in ResolutionErrors.dfy