summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny0/ResolutionErrors.dfy150
-rw-r--r--Test/dafny0/ResolutionErrors.dfy.expect344
2 files changed, 221 insertions, 273 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index d3514b2b..a4161a46 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -150,14 +150,6 @@ class GhostTests {
r := r + g; // fine, for the same reason
r := N(20, 20); // error: call to non-ghost method from ghost method is not okay
}
- ghost method NiceTry()
- ensures false;
- {
- while (true)
-//KRML-confirmed decreases *; // error: not allowed in ghost context
- {
- }
- }
ghost method BreaksAreFineHere(t: int)
{
var n := 0;
@@ -227,8 +219,6 @@ class GhostTests {
label IfNest:
if (p == 67) {
break break; // fine, since this is not a ghost context
- } else if (*) {
-//KRML-confirmed break break break; // error: tries to break out of more loop levels than there are
}
q := q + 1;
}
@@ -363,9 +353,6 @@ method DatatypeDestructors(d: DTD_List) {
ghost var g0 := d.g; // fine
}
}
-method DatatypeDestructors_Ghost(d: DTD_List) {
- var g1 := d.g; // error: cannot use ghost member in non-ghost code//KRML-confirmed
-}
// ------------------- print statements ---------------------------------------
module GhostPrintAttempts {
@@ -435,47 +422,41 @@ method TestCalc(m: int, n: int, a: bool, b: bool)
==> n + m + 2; // error: ==> operator requires boolean lines
}
}
-method TestCalc_Ghost(m: int, n: int, a: bool, b: bool)
-{
- calc {
- n + m;
- { print n + m; } // error: non-ghost statements are not allowed in hints//KRML-confirmed
- m + n;
- }
-}
+
module MyOwnModule {
-class SideEffectChecks {
- ghost var ycalc: int;
+ class SideEffectChecks {
+ ghost var ycalc: int;
- ghost method Mod(a: int)
- modifies this;
- ensures ycalc == a;
- {
- ycalc := a;
- }
+ ghost method Mod(a: int)
+ modifies this;
+ ensures ycalc == a;
+ {
+ ycalc := a;
+ }
- ghost method Bad()
- modifies this;
- ensures 0 == 1;
- {
- var x: int;
- calc {
- 0;
- { Mod(0); } // error: methods with side-effects are not allowed
- ycalc;
- { ycalc := 1; } // error: heap updates are not allowed
- 1;
- { x := 1; } // error: updates to locals defined outside of the hint are not allowed
- x;
- {
- var x: int;
- x := 1; // this is OK
+ ghost method Bad()
+ modifies this;
+ ensures 0 == 1;
+ {
+ var x: int;
+ calc {
+ 0;
+ { Mod(0); } // error: methods with side-effects are not allowed
+ ycalc;
+ { ycalc := 1; } // error: heap updates are not allowed
+ 1;
+ { x := 1; } // error: updates to locals defined outside of the hint are not allowed
+ x;
+ {
+ var x: int;
+ x := 1; // this is OK
+ }
+ 1;
}
- 1;
}
}
}
-}
+
// ------------------- nameless constructors ------------------------------
class YHWH {
@@ -523,14 +504,10 @@ method AssignSuchThatFromGhost()
var x: int;
ghost var g: int;
- x := g; // error: ghost cannot flow into non-ghost//KRML-confirmed
-
x := *;
assume x == g; // this mix of ghosts and non-ghosts is cool (but, of course,
// the compiler will complain)
- x :| x == g; // error: left-side has non-ghost, so RHS must be non-ghost as well//KRML-confirmed
-
x :| assume x == g; // this is cool, since it's an assume (but, of course, the
// compiler will complain)
@@ -603,10 +580,6 @@ method LetSuchThat(ghost z: int, n: nat)
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)
-{
- var x := var y :| y < z; y; // error: contraint depend on ghost (z)//KRML-confirmed
-}
// ------------ quantified variables whose types are not inferred ----------
@@ -677,10 +650,6 @@ module GhostAllocationTests {
5;
{ var y := new G; } // error: 'new' not allowed in ghost contexts
2 + 3;
- { if n != 0 { GhostNew4(n-1); } } // error: cannot call non-ghost method in a ghost context//KRML-confirmed
- 1 + 4;
- { GhostNew5(g); } // error: cannot call method with nonempty modifies//KRML-confirmed
- -5 + 10;
}
}
@@ -730,22 +699,11 @@ module StatementsInExpressions {
{
}
- ghost method M()
- modifies this;
- {
- calc {
- 5;
- { SideEffect(); } // error: cannot call method with side effects//KRML
- 5;
- }
- }
-
function F(): int
{
calc {
6;
{ assert 6 < 8; }
- { NonGhostMethod(); } // error: cannot call non-ghost method//KRML-confirmed
{ var x := 8;
while x != 0
decreases *; // error: cannot use 'decreases *' in a ghost context
@@ -759,12 +717,8 @@ module StatementsInExpressions {
x := x - 1;
}
}
- { MyField := 12; } // error: cannot assign to a field//KRML-confirmed
- { MyGhostField := 12; } // error: cannot assign to any field//KRML-confirmed
- { SideEffect(); } // error: cannot call (ghost) method with a modifies clause//KRML-confirmed
{ var x := 8;
while x != 0
- modifies this; // error: cannot use a modifies clause on a loop//KRML-confirmed
{
x := x - 1;
}
@@ -783,7 +737,6 @@ module StatementsInExpressions {
calc {
6;
{ assert 6 < 8; }
- { NonGhostMethod(); } // error: cannot call non-ghost method//KRML-confirmed
{ var x := 8;
while x != 0
decreases *; // error: cannot use 'decreases *' in a ghost context
@@ -791,12 +744,8 @@ module StatementsInExpressions {
x := x - 1;
}
}
- { MyField := 12; } // error: cannot assign to a field//KRML-confirmed
- { MyGhostField := 12; } // error: cannot assign to any field//KRML-confirmed
- { M(); } // error: cannot call (ghost) method with a modifies clause//KRML-confirmed
{ var x := 8;
while x != 0
- modifies this; // error: cannot use a modifies clause on a loop//KRML-confirmed
{
x := x - 1;
}
@@ -822,7 +771,6 @@ module StatementsInExpressions {
{
MyLemma();
MyGhostMethod(); // error: modifi2es state
- OrdinaryMethod(); // error: not a ghost//KRML-confirmed
OutParamMethod(); // error: has out-parameters
10
}
@@ -1458,9 +1406,9 @@ module GhostTests {
calc {
5;
2 + 3;
- { if n != 0 { GhostNew4(n-1); } } // error: cannot call non-ghost method in a ghost context//ADD:680
+ { if n != 0 { GhostNew4(n-1); } } // error: cannot call non-ghost method in a ghost context
1 + 4;
- { GhostNew5(g); } // error: cannot call method with nonempty modifies//ADD:682
+ { GhostNew5(g); } // error: cannot call method with nonempty modifies
-5 + 10;
}
}
@@ -1485,7 +1433,7 @@ module GhostTests {
{
calc {
5;
- { SideEffect(); } // error: cannot call method with side effects//ADD:738
+ { SideEffect(); } // error: cannot call method with side effects
5;
}
}
@@ -1494,7 +1442,7 @@ module GhostTests {
calc {
6;
{ assert 6 < 8; }
- { NonGhostMethod(); } // error: cannot call non-ghost method//ADD:748
+ { NonGhostMethod(); } // error: cannot call non-ghost method
{ var x := 8;
while x != 0
{
@@ -1507,12 +1455,12 @@ module GhostTests {
x := x - 1;
}
}
- { MyField := 12; } // error: cannot assign to a field, and especially not a non-ghost field//ADD:762
- { MyGhostField := 12; } // error: cannot assign to any field//ADD:763
- { SideEffect(); } // error: cannot call (ghost) method with a modifies clause//ADD:764
+ { MyField := 12; } // error: cannot assign to a field, and especially not a non-ghost field
+ { MyGhostField := 12; } // error: cannot assign to any field
+ { SideEffect(); } // error: cannot call (ghost) method with a modifies clause
{ var x := 8;
while x != 0
- modifies this; // error: cannot use a modifies clause on a loop//ADD:767
+ modifies this; // error: cannot use a modifies clause on a loop
{
x := x - 1;
}
@@ -1529,19 +1477,19 @@ module GhostTests {
calc {
6;
{ assert 6 < 8; }
- { NonGhostMethod(); } // error: cannot call non-ghost method//ADD:786
+ { NonGhostMethod(); } // error: cannot call non-ghost method
{ var x := 8;
while x != 0
{
x := x - 1;
}
}
- { MyField := 12; } // error: cannot assign to a field, and especially not a non-ghost field//ADD:794
- { MyGhostField := 12; } // error: cannot assign to any field//ADD:795
- { M(); } // error: cannot call (ghost) method with a modifies clause//ADD:796
+ { MyField := 12; } // error: cannot assign to a field, and especially not a non-ghost field
+ { MyGhostField := 12; } // error: cannot assign to any field
+ { M(); } // error: cannot call (ghost) method with a modifies clause
{ var x := 8;
while x != 0
- modifies this; // error: cannot use a modifies clause on a loop//ADD:799
+ modifies this; // error: cannot use a modifies clause on a loop
{
x := x - 1;
}
@@ -1565,7 +1513,7 @@ module GhostTests {
function UseLemma(): int
{
MyLemma();
- OrdinaryMethod(); // error: not a ghost//ADD:825
+ OrdinaryMethod(); // error: not a ghost
10
}
}
@@ -1576,7 +1524,7 @@ module EvenMoreGhostTests {
ensures false;
{
while (true)
- decreases *; // error: not allowed in ghost context//ADD:157
+ decreases *; // error: not allowed in ghost context
{
}
}
@@ -1594,7 +1542,7 @@ module EvenMoreGhostTests {
if (p == 67) {
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//ADD:231
+ break break break; // error: tries to break out of more loop levels than there are
}
}
}
@@ -1620,20 +1568,20 @@ module BadGhostTransfer {
datatype DTD_List = DTD_Nil | DTD_Cons(Car: int, Cdr: DTD_List, ghost g: int)
method DatatypeDestructors_Ghost(d: DTD_List) {
- var g1 := d.g; // error: cannot use ghost member in non-ghost code//ADD:367
+ var g1 := d.g; // error: cannot use ghost member in non-ghost code
}
method AssignSuchThatFromGhost()
{
var x: int;
ghost var g: int;
- x := g; // error: ghost cannot flow into non-ghost//ADD:526
+ x := g; // error: ghost cannot flow into non-ghost
x := *;
assume x == g; // this mix of ghosts and non-ghosts is cool (but, of course,
// the compiler will complain)
- x :| x == g; // error: left-side has non-ghost, so RHS must be non-ghost as well//ADD:532
+ x :| x == g; // error: left-side has non-ghost, so RHS must be non-ghost as well
x :| assume x == g; // this is cool, since it's an assume (but, of course, the
// compiler will complain)
@@ -1650,7 +1598,7 @@ module MoreGhostPrintAttempts {
{
calc {
n + m;
- { print n + m; } // error: non-ghost statements are not allowed in hints//ADD:442
+ { print n + m; } // error: non-ghost statements are not allowed in hints
m + n;
}
}
@@ -1659,6 +1607,6 @@ module MoreGhostPrintAttempts {
module MoreLetSuchThatExpr {
method LetSuchThat_Ghost(ghost z: int, n: nat)
{
- var x := var y :| y < z; y; // error: contraint depend on ghost (z)//ADD:608
+ var x := var y :| y < z; y; // error: contraint depend on ghost (z)
}
}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index ee2dd5f7..e5506688 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -8,152 +8,152 @@ ResolutionErrors.dfy(137,4): Error: ghost variables are allowed only in specific
ResolutionErrors.dfy(141,21): Error: ghost variables are allowed only in specification contexts
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(251,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
-ResolutionErrors.dfy(274,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(288,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(293,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
-ResolutionErrors.dfy(375,15): Error: ghost variables are allowed only in specification contexts
-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(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(678,17): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(700,21): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(751,22): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(789,22): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(824,19): Error: calls to methods with side-effects are not allowed inside a statement expression
-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: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
-ResolutionErrors.dfy(1178,24): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile 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(1488,20): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(1510,18): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(1511,23): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(1512,20): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(1515,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(1497,24): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(1510,18): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ResolutionErrors.dfy(1539,18): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(1540,23): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(1541,11): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(1544,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(1532,24): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(1539,18): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ResolutionErrors.dfy(1568,20): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(1461,29): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(1463,17): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(1579,16): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(1597,12): Error: trying to break out of more loop levels than there are enclosing loops
-ResolutionErrors.dfy(1623,16): Error: ghost fields are allowed only in specification contexts
-ResolutionErrors.dfy(1630,9): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(1636,4): Error: non-ghost variable cannot be assigned a value that depends on a ghost
-ResolutionErrors.dfy(1653,8): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ResolutionErrors.dfy(1662,26): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(488,2): Error: More than one anonymous constructor
+ResolutionErrors.dfy(241,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(264,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(278,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(283,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
+ResolutionErrors.dfy(362,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(444,13): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(446,16): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(448,12): Error: a hint is not allowed to update a variable declared outside the hint
+ResolutionErrors.dfy(535,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
+ResolutionErrors.dfy(540,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
+ResolutionErrors.dfy(554,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
+ResolutionErrors.dfy(566,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree
+ResolutionErrors.dfy(592,25): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(592,23): Error: type variable 'T' in the function call to 'P' could not be determined
+ResolutionErrors.dfy(599,25): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(599,23): Error: type variable 'T' in the function call to 'P' could not be determined
+ResolutionErrors.dfy(612,13): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(613,9): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(620,14): Error: new allocation not supported in forall statements
+ResolutionErrors.dfy(625,11): Error: the body of the enclosing forall statement is not allowed to update heap locations
+ResolutionErrors.dfy(625,14): Error: new allocation not allowed in ghost context
+ResolutionErrors.dfy(635,23): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(642,15): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(651,17): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(669,21): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(709,22): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(742,22): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(773,19): Error: calls to methods with side-effects are not allowed inside a statement expression
+ResolutionErrors.dfy(774,20): Error: wrong number of method result arguments (got 0, expected 1)
+ResolutionErrors.dfy(786,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(796,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(807,36): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(816,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(830,6): Error: RHS (of type B) not assignable to LHS (of type object)
+ResolutionErrors.dfy(831,6): Error: RHS (of type int) not assignable to LHS (of type object)
+ResolutionErrors.dfy(832,6): Error: RHS (of type B) not assignable to LHS (of type object)
+ResolutionErrors.dfy(837,6): Error: RHS (of type G) not assignable to LHS (of type object)
+ResolutionErrors.dfy(838,6): Error: RHS (of type Dt) not assignable to LHS (of type object)
+ResolutionErrors.dfy(839,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)
+ResolutionErrors.dfy(901,4): Error: LHS of array assignment must denote an array element (found seq<int>)
+ResolutionErrors.dfy(902,4): Error: LHS of array assignment must denote an array element (found seq<int>)
+ResolutionErrors.dfy(907,10): Error: LHS of assignment must denote a mutable field
+ResolutionErrors.dfy(908,10): Error: LHS of assignment must denote a mutable field
+ResolutionErrors.dfy(909,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(910,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(911,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(912,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(993,11): Error: Wrong number of type arguments (2 instead of 1) passed to array type: array3
+ResolutionErrors.dfy(994,11): Error: Wrong number of type arguments (2 instead of 1) passed to class: C
+ResolutionErrors.dfy(1005,7): Error: Duplicate name of top-level declaration: BadSyn2
+ResolutionErrors.dfy(1002,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List
+ResolutionErrors.dfy(1003,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(1004,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(1011,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A
+ResolutionErrors.dfy(1014,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1018,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1027,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
+ResolutionErrors.dfy(1030,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1035,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1054,21): Error: unresolved identifier: x
+ResolutionErrors.dfy(1061,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
+ResolutionErrors.dfy(1073,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(1083,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)
+ResolutionErrors.dfy(1088,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)
+ResolutionErrors.dfy(1093,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)
+ResolutionErrors.dfy(1094,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)
+ResolutionErrors.dfy(1099,13): Error: arguments must have the same type (got P<int> and P<X>)
+ResolutionErrors.dfy(1100,13): Error: arguments must have the same type (got P<bool> and P<X>)
+ResolutionErrors.dfy(1101,13): Error: arguments must have the same type (got P<int> and P<bool>)
+ResolutionErrors.dfy(1124,38): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
+ResolutionErrors.dfy(1126,24): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
+ResolutionErrors.dfy(1231,26): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1232,31): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1233,29): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1243,34): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1259,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(1260,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(1297,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
+ResolutionErrors.dfy(1307,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1335,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(1345,29): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1347,49): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1347,54): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1368,11): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1368,16): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1369,11): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1369,16): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1370,11): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1370,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(1371,11): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1371,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(1376,16): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1376,13): Error: arguments must have the same type (got int and #type)
+ResolutionErrors.dfy(1377,16): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1377,13): Error: arguments must have the same type (got int and #module)
+ResolutionErrors.dfy(1378,4): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1379,4): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1388,11): Error: type of RHS of assign-such-that statement must be boolean (got int)
+ResolutionErrors.dfy(1389,9): Error: type of RHS of assign-such-that statement must be boolean (got int)
+ResolutionErrors.dfy(1390,13): Error: type of RHS of assign-such-that statement must be boolean (got int)
+ResolutionErrors.dfy(1393,15): Error: type of RHS of let-such-that expression must be boolean (got int)
+ResolutionErrors.dfy(1436,20): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1458,18): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1459,23): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1460,20): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1463,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(1445,24): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1458,18): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(1487,18): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1488,23): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1489,11): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1492,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(1480,24): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1487,18): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(1516,20): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1409,29): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1411,17): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1527,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(1545,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(1571,16): Error: ghost fields are allowed only in specification contexts
+ResolutionErrors.dfy(1578,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1584,4): Error: non-ghost variable cannot be assigned a value that depends on a ghost
+ResolutionErrors.dfy(1601,8): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(1610,26): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(469,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')
ResolutionErrors.dfy(93,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(95,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(97,18): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)
-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(475,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
+ResolutionErrors.dfy(480,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
+ResolutionErrors.dfy(481,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
+ResolutionErrors.dfy(483,9): Error: class Lamb does not have an anonymous constructor
+ResolutionErrors.dfy(850,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
+ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(857,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(865,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(875,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(886,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1042,23): Error: unresolved identifier: x
+ResolutionErrors.dfy(1045,20): Error: unresolved identifier: x
+ResolutionErrors.dfy(1048,23): Error: unresolved identifier: x
+ResolutionErrors.dfy(1050,19): Error: unresolved identifier: x
+ResolutionErrors.dfy(1052,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>)
@@ -167,36 +167,36 @@ 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(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(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(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
+ResolutionErrors.dfy(301,4): Error: label shadows an enclosing label
+ResolutionErrors.dfy(306,2): Error: duplicate label
+ResolutionErrors.dfy(332,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(333,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(335,9): Error: a constructor is allowed to be called only when an object is being allocated
+ResolutionErrors.dfy(349,16): Error: arguments must have the same type (got int and DTD_List)
+ResolutionErrors.dfy(350,16): Error: arguments must have the same type (got DTD_List and int)
+ResolutionErrors.dfy(351,25): Error: arguments must have the same type (got bool and int)
+ResolutionErrors.dfy(387,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
+ResolutionErrors.dfy(399,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
+ResolutionErrors.dfy(407,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
+ResolutionErrors.dfy(412,6): Error: all lines in a calculation must have the same type (got int after bool)
+ResolutionErrors.dfy(415,6): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(415,6): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(416,10): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(416,10): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(421,10): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(421,10): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(580,18): Error: unresolved identifier: w
+ResolutionErrors.dfy(683,11): Error: lemmas are not allowed to have modifies clauses
+ResolutionErrors.dfy(924,9): Error: unresolved identifier: s
+ResolutionErrors.dfy(935,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
+ResolutionErrors.dfy(936,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
+ResolutionErrors.dfy(942,16): Error: condition is expected to be of type bool, but is int
+ResolutionErrors.dfy(943,16): Error: member 3 does not exist in datatype _tuple#3
+ResolutionErrors.dfy(943,26): Error: member x does not exist in datatype _tuple#2
+ResolutionErrors.dfy(966,15): Error: arguments to / must have the same type (got real and int)
+ResolutionErrors.dfy(967,10): Error: second argument to % must be of type int (instead got real)
+ResolutionErrors.dfy(1112,8): Error: new cannot be applied to a trait
+ResolutionErrors.dfy(1133,13): Error: first argument to / must be of numeric type (instead got set<bool>)
+ResolutionErrors.dfy(1140,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(1155,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
201 resolution/type errors detected in ResolutionErrors.dfy
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-20 19:39:17 +0000