From 4c21d765625b35eab9f5dc4ca21f170d3f7a2f04 Mon Sep 17 00:00:00 2001 From: leino Date: Mon, 28 Sep 2015 13:27:22 -0700 Subject: Whitespace changes in test file --- Test/dafny0/ResolutionErrors.dfy | 150 +++++--------- Test/dafny0/ResolutionErrors.dfy.expect | 344 ++++++++++++++++---------------- 2 files changed, 221 insertions(+), 273 deletions(-) (limited to 'Test/dafny0') 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) not assignable to LHS (of type List) -ResolutionErrors.dfy(563,7): Error: RHS (of type List) not assignable to LHS (of type List) -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) -ResolutionErrors.dfy(954,4): Error: LHS of array assignment must denote an array element (found seq) -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) not assignable to LHS (of type P) -ResolutionErrors.dfy(1140,6): Error: RHS (of type P) not assignable to LHS (of type P) -ResolutionErrors.dfy(1145,6): Error: RHS (of type P) not assignable to LHS (of type P) -ResolutionErrors.dfy(1146,6): Error: RHS (of type P) not assignable to LHS (of type P) -ResolutionErrors.dfy(1151,13): Error: arguments must have the same type (got P and P) -ResolutionErrors.dfy(1152,13): Error: arguments must have the same type (got P and P) -ResolutionErrors.dfy(1153,13): Error: arguments must have the same type (got P and P) -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) -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) -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) not assignable to LHS (of type List) +ResolutionErrors.dfy(540,7): Error: RHS (of type List) not assignable to LHS (of type List) +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) +ResolutionErrors.dfy(902,4): Error: LHS of array assignment must denote an array element (found seq) +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) not assignable to LHS (of type P) +ResolutionErrors.dfy(1088,6): Error: RHS (of type P) not assignable to LHS (of type P) +ResolutionErrors.dfy(1093,6): Error: RHS (of type P) not assignable to LHS (of type P) +ResolutionErrors.dfy(1094,6): Error: RHS (of type P) not assignable to LHS (of type P) +ResolutionErrors.dfy(1099,13): Error: arguments must have the same type (got P and P) +ResolutionErrors.dfy(1100,13): Error: arguments must have the same type (got P and P) +ResolutionErrors.dfy(1101,13): Error: arguments must have the same type (got P and P) +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) +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) +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) ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3) @@ -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, got GenericClass) -ResolutionErrors.dfy(412,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList) -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) -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, got GenericClass) +ResolutionErrors.dfy(399,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList) +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) +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 -- cgit v1.2.3