Changes that only affect line numbers in test case

2 files changed, 231 insertions, 173 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index d34fd8a5..d38d2506 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -195,7 +195,6 @@ class GhostTests {
       decreases 112 - n;

     {

       label MyStructure: {

-//KRML(ghost)        if (k % 17 == 0) { break MyStructure; }  // error: break from ghost to non-ghost point

         k := k + 1;

       }

       label MyOtherStructure:

@@ -218,7 +217,6 @@ class GhostTests {
               case true => break LoopLabel1;  // fine

             }

           } else if (m % 101 == 0) {

-//KRML(ghost)            break break;  // error: break out of non-ghost loop from ghost context

           }

           m := m + 3;

         }

@@ -231,20 +229,73 @@ class GhostTests {
             break break;  // fine, since this is not a ghost context

           } else if (*) {

             break break break;  // error: tries to break out of more loop levels than there are

+          }

+          q := q + 1;

+        }

+      } else if (n == t) {

+      }

+      n := n + 1;

+      p := p + 1;

+    }

+  }

+/***KRML  method BreakMayNotBeFineHere_Ghost(ghost t: int)

+  {

+    var n := 0;

+    ghost var k := 0;

+    var p := 0;

+    while (true)

+      invariant n <= 112;

+      decreases 112 - n;

+    {

+      label MyStructure: {

+        if (k % 17 == 0) { break MyStructure; }  // error: break from ghost to non-ghost point

+        k := k + 1;

+      }

+      label MyOtherStructure:

+      if (k % 17 == 0) {

+        break MyOtherStructure;  // this break is fine

+      } else {

+        k := k + 1;

+      }

+

+      var dontKnow;

+      if (n == 112) {

+        ghost var m := 0;

+        label LoopLabel0:

+        label LoopLabel1:

+        while (m < 200) {

+          if (m % 103 == 0) {

+            if {

+              case true => break;  // fine, since this breaks out of the enclosing ghost loop

+              case true => break LoopLabel0;  // fine

+              case true => break LoopLabel1;  // fine

+            }

+          } else if (m % 101 == 0) {

+            break break;  // error: break out of non-ghost loop from ghost context

+          }

+          m := m + 3;

+        }

+        break;

+      } else if (dontKnow == 708) {

+        var q := 0;

+        while (q < 1) {

+          label IfNest:

+          if (p == 67) {

+            break break;  // fine, since this is not a ghost context

           } else if (*) {

-//KRML(ghost)            break break;  // fine, since this is not a ghost context

+            break break;  // fine, since this is not a ghost context

           } else if (k == 67) {

-//KRML(ghost)            break break;  // error, because this is a ghost context

+            break break;  // error, because this is a ghost context

           }

           q := q + 1;

         }

       } else if (n == t) {

-//KRML(ghost)        return;  // error: this is a ghost context trying to return from a non-ghost method

+        return;  // error: this is a ghost context trying to return from a non-ghost method

       }

       n := n + 1;

       p := p + 1;

     }

-  }

+  }****/

 }

 

 method DuplicateLabels(n: int) {

@@ -310,9 +361,11 @@ method DatatypeDestructors(d: DTD_List) {
       assert d.DTD_Cons? == d.Car;  // type error

       assert d == DTD_Cons(hd, tl, 5);

       ghost var g0 := d.g;  // fine

-//KRML(ghost)      var g1 := d.g;  // error: cannot use ghost member in non-ghost code

   }

 }

+method DatatypeDestructors_Ghost(d: DTD_List) {

+//KRML  var g1 := d.g;  // error: cannot use ghost member in non-ghost code

+}

 

 // ------------------- print statements ---------------------------------------

 

@@ -381,9 +434,12 @@ method TestCalc(m: int, n: int, a: bool, b: bool)
     n + m + 1;

     ==> n + m + 2; // error: ==> operator requires boolean lines

   }

+}

+method TestCalc_Ghost(m: int, n: int, a: bool, b: bool)

+{

   calc {

     n + m;

-//KRML(ghost)    { print n + m; } // error: non-ghost statements are not allowed in hints

+//KRML    { print n + m; } // error: non-ghost statements are not allowed in hints

     m + n;

   }

 }

@@ -543,12 +599,14 @@ method LetSuchThat(ghost z: int, n: nat)
   var x: int;

   x := var y :| y < 0; y;  // fine for the resolver (but would give a verification error for not being deterministic)

 

-//KRML(ghost)  x := var y :| y < z; y;  // error: contraint depend on ghost (z)

-

   x := var w :| w == 2*w; w;  // fine (even for the verifier, this one)

   x := var w := 2*w; w;  // error: the 'w' in the RHS of the assignment is not in scope

   ghost var xg := var w :| w == 2*w; w;

 }

+method LetSuchThat_Ghost(ghost z: int, n: nat)

+{

+//KRML  var x := var y :| y < z; y;  // error: contraint depend on ghost (z)

+}

 

 // ------------ quantified variables whose types are not inferred ----------

 

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 04913cf5..55d2e79c 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -1,112 +1,112 @@
-ResolutionErrors.dfy(502,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

-ResolutionErrors.dfy(507,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

-ResolutionErrors.dfy(521,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)

-ResolutionErrors.dfy(533,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree

-ResolutionErrors.dfy(561,25): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(561,23): Error: type variable 'T' in the function call to 'P' could not be determined

-ResolutionErrors.dfy(568,25): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(568,23): Error: type variable 'T' in the function call to 'P' could not be determined

-ResolutionErrors.dfy(581,13): Error: 'new' is not allowed in ghost contexts

-ResolutionErrors.dfy(582,9): Error: 'new' is not allowed in ghost contexts

-ResolutionErrors.dfy(589,14): Error: new allocation not supported in forall statements

-ResolutionErrors.dfy(594,11): Error: the body of the enclosing forall statement is not allowed to update heap locations

-ResolutionErrors.dfy(594,14): Error: new allocation not allowed in ghost context

-ResolutionErrors.dfy(604,23): Error: 'new' is not allowed in ghost contexts

-ResolutionErrors.dfy(611,15): Error: 'new' is not allowed in ghost contexts

-ResolutionErrors.dfy(611,15): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(620,17): Error: 'new' is not allowed in ghost contexts

-ResolutionErrors.dfy(622,29): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(624,17): Error: calls to methods with side-effects are not allowed inside a hint

-ResolutionErrors.dfy(642,21): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(680,20): Error: calls to methods with side-effects are not allowed inside a hint

-ResolutionErrors.dfy(690,24): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(693,22): Error: 'decreases *' is not allowed on ghost loops

-ResolutionErrors.dfy(704,18): Error: a hint is not allowed to update heap locations

-ResolutionErrors.dfy(705,23): Error: a hint is not allowed to update heap locations

-ResolutionErrors.dfy(706,20): Error: calls to methods with side-effects are not allowed inside a hint

-ResolutionErrors.dfy(709,21): Error: a while statement used inside a hint is not allowed to have a modifies clause

-ResolutionErrors.dfy(728,24): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(731,22): Error: 'decreases *' is not allowed on ghost loops

-ResolutionErrors.dfy(736,18): Error: a hint is not allowed to update heap locations

-ResolutionErrors.dfy(737,23): Error: a hint is not allowed to update heap locations

-ResolutionErrors.dfy(738,11): Error: calls to methods with side-effects are not allowed inside a hint

-ResolutionErrors.dfy(741,21): Error: a while statement used inside a hint is not allowed to have a modifies clause

-ResolutionErrors.dfy(766,19): Error: calls to methods with side-effects are not allowed inside a statement expression

-ResolutionErrors.dfy(767,20): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(768,20): Error: wrong number of method result arguments (got 0, expected 1)

-ResolutionErrors.dfy(780,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

-ResolutionErrors.dfy(790,4): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(801,36): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(810,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

-ResolutionErrors.dfy(824,6): Error: RHS (of type B) not assignable to LHS (of type object)

-ResolutionErrors.dfy(825,6): Error: RHS (of type int) not assignable to LHS (of type object)

-ResolutionErrors.dfy(826,6): Error: RHS (of type B) not assignable to LHS (of type object)

-ResolutionErrors.dfy(831,6): Error: RHS (of type G) not assignable to LHS (of type object)

-ResolutionErrors.dfy(832,6): Error: RHS (of type Dt) not assignable to LHS (of type object)

-ResolutionErrors.dfy(833,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)

-ResolutionErrors.dfy(895,4): Error: LHS of array assignment must denote an array element (found seq<int>)

-ResolutionErrors.dfy(896,4): Error: LHS of array assignment must denote an array element (found seq<int>)

-ResolutionErrors.dfy(901,10): Error: LHS of assignment must denote a mutable field

-ResolutionErrors.dfy(902,10): Error: LHS of assignment must denote a mutable field

-ResolutionErrors.dfy(903,9): Error: cannot assign to a range of array elements (try the 'forall' statement)

-ResolutionErrors.dfy(904,9): Error: cannot assign to a range of array elements (try the 'forall' statement)

-ResolutionErrors.dfy(905,5): Error: cannot assign to a range of array elements (try the 'forall' statement)

-ResolutionErrors.dfy(906,5): Error: cannot assign to a range of array elements (try the 'forall' statement)

-ResolutionErrors.dfy(987,11): Error: Wrong number of type arguments (2 instead of 1) passed to array type: array3

-ResolutionErrors.dfy(988,11): Error: Wrong number of type arguments (2 instead of 1) passed to class: C

-ResolutionErrors.dfy(999,7): Error: Duplicate name of top-level declaration: BadSyn2

-ResolutionErrors.dfy(996,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List

-ResolutionErrors.dfy(997,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name or declare a module import 'opened?')

-ResolutionErrors.dfy(998,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

-ResolutionErrors.dfy(1005,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A

-ResolutionErrors.dfy(1008,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

-ResolutionErrors.dfy(1012,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

-ResolutionErrors.dfy(1021,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed

-ResolutionErrors.dfy(1024,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

-ResolutionErrors.dfy(1029,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

-ResolutionErrors.dfy(1048,21): Error: unresolved identifier: x

-ResolutionErrors.dfy(1055,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P

-ResolutionErrors.dfy(1067,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name or declare a module import 'opened?')

-ResolutionErrors.dfy(1077,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)

-ResolutionErrors.dfy(1082,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)

-ResolutionErrors.dfy(1087,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)

-ResolutionErrors.dfy(1088,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)

-ResolutionErrors.dfy(1093,13): Error: arguments must have the same type (got P<int> and P<X>)

-ResolutionErrors.dfy(1094,13): Error: arguments must have the same type (got P<bool> and P<X>)

-ResolutionErrors.dfy(1095,13): Error: arguments must have the same type (got P<int> and P<bool>)

-ResolutionErrors.dfy(1118,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'

-ResolutionErrors.dfy(1120,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'

-ResolutionErrors.dfy(1225,26): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(1226,31): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(1227,29): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(1237,34): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(1253,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

-ResolutionErrors.dfy(1254,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

-ResolutionErrors.dfy(1291,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)

-ResolutionErrors.dfy(1301,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

-ResolutionErrors.dfy(1329,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)

-ResolutionErrors.dfy(1339,29): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(1341,49): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(1341,54): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(1362,11): Error: name of type (X) is used as a variable

-ResolutionErrors.dfy(1362,16): Error: name of type (X) is used as a variable

-ResolutionErrors.dfy(1363,11): Error: name of module (Y) is used as a variable

-ResolutionErrors.dfy(1363,16): Error: name of module (Y) is used as a variable

-ResolutionErrors.dfy(1364,11): Error: name of type (X) is used as a variable

-ResolutionErrors.dfy(1364,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #type, or a map with domain #type (instead got map<real, string>)

-ResolutionErrors.dfy(1365,11): Error: name of module (Y) is used as a variable

-ResolutionErrors.dfy(1365,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #module, or a map with domain #module (instead got map<real, string>)

-ResolutionErrors.dfy(1370,16): Error: name of type (X) is used as a variable

-ResolutionErrors.dfy(1370,13): Error: arguments must have the same type (got int and #type)

-ResolutionErrors.dfy(1371,16): Error: name of module (Y) is used as a variable

-ResolutionErrors.dfy(1371,13): Error: arguments must have the same type (got int and #module)

-ResolutionErrors.dfy(1372,4): Error: name of type (X) is used as a variable

-ResolutionErrors.dfy(1373,4): Error: name of module (Y) is used as a variable

-ResolutionErrors.dfy(1382,11): Error: type of RHS of assign-such-that statement must be boolean (got int)

-ResolutionErrors.dfy(1383,9): Error: type of RHS of assign-such-that statement must be boolean (got int)

-ResolutionErrors.dfy(1384,13): Error: type of RHS of assign-such-that statement must be boolean (got int)

-ResolutionErrors.dfy(1387,15): Error: type of RHS of let-such-that expression must be boolean (got int)

-ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor

+ResolutionErrors.dfy(558,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

+ResolutionErrors.dfy(563,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

+ResolutionErrors.dfy(577,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)

+ResolutionErrors.dfy(589,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree

+ResolutionErrors.dfy(619,25): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(619,23): Error: type variable 'T' in the function call to 'P' could not be determined

+ResolutionErrors.dfy(626,25): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(626,23): Error: type variable 'T' in the function call to 'P' could not be determined

+ResolutionErrors.dfy(639,13): Error: 'new' is not allowed in ghost contexts

+ResolutionErrors.dfy(640,9): Error: 'new' is not allowed in ghost contexts

+ResolutionErrors.dfy(647,14): Error: new allocation not supported in forall statements

+ResolutionErrors.dfy(652,11): Error: the body of the enclosing forall statement is not allowed to update heap locations

+ResolutionErrors.dfy(652,14): Error: new allocation not allowed in ghost context

+ResolutionErrors.dfy(662,23): Error: 'new' is not allowed in ghost contexts

+ResolutionErrors.dfy(669,15): Error: 'new' is not allowed in ghost contexts

+ResolutionErrors.dfy(669,15): Error: only ghost methods can be called from this context

+ResolutionErrors.dfy(678,17): Error: 'new' is not allowed in ghost contexts

+ResolutionErrors.dfy(680,29): Error: only ghost methods can be called from this context

+ResolutionErrors.dfy(682,17): Error: calls to methods with side-effects are not allowed inside a hint

+ResolutionErrors.dfy(700,21): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(738,20): Error: calls to methods with side-effects are not allowed inside a hint

+ResolutionErrors.dfy(748,24): Error: only ghost methods can be called from this context

+ResolutionErrors.dfy(751,22): Error: 'decreases *' is not allowed on ghost loops

+ResolutionErrors.dfy(762,18): Error: a hint is not allowed to update heap locations

+ResolutionErrors.dfy(763,23): Error: a hint is not allowed to update heap locations

+ResolutionErrors.dfy(764,20): Error: calls to methods with side-effects are not allowed inside a hint

+ResolutionErrors.dfy(767,21): Error: a while statement used inside a hint is not allowed to have a modifies clause

+ResolutionErrors.dfy(786,24): Error: only ghost methods can be called from this context

+ResolutionErrors.dfy(789,22): Error: 'decreases *' is not allowed on ghost loops

+ResolutionErrors.dfy(794,18): Error: a hint is not allowed to update heap locations

+ResolutionErrors.dfy(795,23): Error: a hint is not allowed to update heap locations

+ResolutionErrors.dfy(796,11): Error: calls to methods with side-effects are not allowed inside a hint

+ResolutionErrors.dfy(799,21): Error: a while statement used inside a hint is not allowed to have a modifies clause

+ResolutionErrors.dfy(824,19): Error: calls to methods with side-effects are not allowed inside a statement expression

+ResolutionErrors.dfy(825,20): Error: only ghost methods can be called from this context

+ResolutionErrors.dfy(826,20): Error: wrong number of method result arguments (got 0, expected 1)

+ResolutionErrors.dfy(838,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

+ResolutionErrors.dfy(848,4): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(859,36): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(868,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

+ResolutionErrors.dfy(882,6): Error: RHS (of type B) not assignable to LHS (of type object)

+ResolutionErrors.dfy(883,6): Error: RHS (of type int) not assignable to LHS (of type object)

+ResolutionErrors.dfy(884,6): Error: RHS (of type B) not assignable to LHS (of type object)

+ResolutionErrors.dfy(889,6): Error: RHS (of type G) not assignable to LHS (of type object)

+ResolutionErrors.dfy(890,6): Error: RHS (of type Dt) not assignable to LHS (of type object)

+ResolutionErrors.dfy(891,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)

+ResolutionErrors.dfy(953,4): Error: LHS of array assignment must denote an array element (found seq<int>)

+ResolutionErrors.dfy(954,4): Error: LHS of array assignment must denote an array element (found seq<int>)

+ResolutionErrors.dfy(959,10): Error: LHS of assignment must denote a mutable field

+ResolutionErrors.dfy(960,10): Error: LHS of assignment must denote a mutable field

+ResolutionErrors.dfy(961,9): Error: cannot assign to a range of array elements (try the 'forall' statement)

+ResolutionErrors.dfy(962,9): Error: cannot assign to a range of array elements (try the 'forall' statement)

+ResolutionErrors.dfy(963,5): Error: cannot assign to a range of array elements (try the 'forall' statement)

+ResolutionErrors.dfy(964,5): Error: cannot assign to a range of array elements (try the 'forall' statement)

+ResolutionErrors.dfy(1045,11): Error: Wrong number of type arguments (2 instead of 1) passed to array type: array3

+ResolutionErrors.dfy(1046,11): Error: Wrong number of type arguments (2 instead of 1) passed to class: C

+ResolutionErrors.dfy(1057,7): Error: Duplicate name of top-level declaration: BadSyn2

+ResolutionErrors.dfy(1054,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List

+ResolutionErrors.dfy(1055,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name or declare a module import 'opened?')

+ResolutionErrors.dfy(1056,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

+ResolutionErrors.dfy(1063,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A

+ResolutionErrors.dfy(1066,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

+ResolutionErrors.dfy(1070,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

+ResolutionErrors.dfy(1079,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed

+ResolutionErrors.dfy(1082,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

+ResolutionErrors.dfy(1087,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

+ResolutionErrors.dfy(1106,21): Error: unresolved identifier: x

+ResolutionErrors.dfy(1113,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P

+ResolutionErrors.dfy(1125,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name or declare a module import 'opened?')

+ResolutionErrors.dfy(1135,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)

+ResolutionErrors.dfy(1140,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)

+ResolutionErrors.dfy(1145,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)

+ResolutionErrors.dfy(1146,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)

+ResolutionErrors.dfy(1151,13): Error: arguments must have the same type (got P<int> and P<X>)

+ResolutionErrors.dfy(1152,13): Error: arguments must have the same type (got P<bool> and P<X>)

+ResolutionErrors.dfy(1153,13): Error: arguments must have the same type (got P<int> and P<bool>)

+ResolutionErrors.dfy(1176,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'

+ResolutionErrors.dfy(1178,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'

+ResolutionErrors.dfy(1283,26): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1284,31): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1285,29): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1295,34): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1311,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

+ResolutionErrors.dfy(1312,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

+ResolutionErrors.dfy(1349,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)

+ResolutionErrors.dfy(1359,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

+ResolutionErrors.dfy(1387,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)

+ResolutionErrors.dfy(1397,29): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(1399,49): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(1399,54): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(1420,11): Error: name of type (X) is used as a variable

+ResolutionErrors.dfy(1420,16): Error: name of type (X) is used as a variable

+ResolutionErrors.dfy(1421,11): Error: name of module (Y) is used as a variable

+ResolutionErrors.dfy(1421,16): Error: name of module (Y) is used as a variable

+ResolutionErrors.dfy(1422,11): Error: name of type (X) is used as a variable

+ResolutionErrors.dfy(1422,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #type, or a map with domain #type (instead got map<real, string>)

+ResolutionErrors.dfy(1423,11): Error: name of module (Y) is used as a variable

+ResolutionErrors.dfy(1423,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #module, or a map with domain #module (instead got map<real, string>)

+ResolutionErrors.dfy(1428,16): Error: name of type (X) is used as a variable

+ResolutionErrors.dfy(1428,13): Error: arguments must have the same type (got int and #type)

+ResolutionErrors.dfy(1429,16): Error: name of module (Y) is used as a variable

+ResolutionErrors.dfy(1429,13): Error: arguments must have the same type (got int and #module)

+ResolutionErrors.dfy(1430,4): Error: name of type (X) is used as a variable

+ResolutionErrors.dfy(1431,4): Error: name of module (Y) is used as a variable

+ResolutionErrors.dfy(1440,11): Error: type of RHS of assign-such-that statement must be boolean (got int)

+ResolutionErrors.dfy(1441,9): Error: type of RHS of assign-such-that statement must be boolean (got int)

+ResolutionErrors.dfy(1442,13): Error: type of RHS of assign-such-that statement must be boolean (got int)

+ResolutionErrors.dfy(1445,15): Error: type of RHS of let-such-that expression must be boolean (got int)

+ResolutionErrors.dfy(488,2): Error: More than one anonymous constructor

 ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')

 ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

@@ -124,25 +124,25 @@ ResolutionErrors.dfy(141,21): Error: ghost variables are allowed only in specifi
 ResolutionErrors.dfy(142,35): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(151,10): Error: only ghost methods can be called from this context

 ResolutionErrors.dfy(157,16): Error: 'decreases *' is not allowed on ghost loops

-ResolutionErrors.dfy(233,12): Error: trying to break out of more loop levels than there are enclosing loops

-ResolutionErrors.dfy(408,11): Error: calls to methods with side-effects are not allowed inside a hint

-ResolutionErrors.dfy(410,14): Error: a hint is not allowed to update heap locations

-ResolutionErrors.dfy(412,10): Error: a hint is not allowed to update a variable declared outside the hint

-ResolutionErrors.dfy(438,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called

-ResolutionErrors.dfy(443,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

-ResolutionErrors.dfy(444,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

-ResolutionErrors.dfy(446,9): Error: class Lamb does not have an anonymous constructor

-ResolutionErrors.dfy(844,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)

-ResolutionErrors.dfy(848,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

-ResolutionErrors.dfy(851,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

-ResolutionErrors.dfy(859,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

-ResolutionErrors.dfy(869,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

-ResolutionErrors.dfy(880,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

-ResolutionErrors.dfy(1036,23): Error: unresolved identifier: x

-ResolutionErrors.dfy(1039,20): Error: unresolved identifier: x

-ResolutionErrors.dfy(1042,23): Error: unresolved identifier: x

-ResolutionErrors.dfy(1044,19): Error: unresolved identifier: x

-ResolutionErrors.dfy(1046,19): Error: unresolved identifier: x

+ResolutionErrors.dfy(231,12): Error: trying to break out of more loop levels than there are enclosing loops

+ResolutionErrors.dfy(464,11): Error: calls to methods with side-effects are not allowed inside a hint

+ResolutionErrors.dfy(466,14): Error: a hint is not allowed to update heap locations

+ResolutionErrors.dfy(468,10): Error: a hint is not allowed to update a variable declared outside the hint

+ResolutionErrors.dfy(494,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called

+ResolutionErrors.dfy(499,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

+ResolutionErrors.dfy(500,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

+ResolutionErrors.dfy(502,9): Error: class Lamb does not have an anonymous constructor

+ResolutionErrors.dfy(902,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)

+ResolutionErrors.dfy(906,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

+ResolutionErrors.dfy(909,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

+ResolutionErrors.dfy(917,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

+ResolutionErrors.dfy(927,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

+ResolutionErrors.dfy(938,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

+ResolutionErrors.dfy(1094,23): Error: unresolved identifier: x

+ResolutionErrors.dfy(1097,20): Error: unresolved identifier: x

+ResolutionErrors.dfy(1100,23): Error: unresolved identifier: x

+ResolutionErrors.dfy(1102,19): Error: unresolved identifier: x

+ResolutionErrors.dfy(1104,19): Error: unresolved identifier: x

 ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops

 ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3<T>)

 ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3<T>)

@@ -156,39 +156,39 @@ ResolutionErrors.dfy(62,14): Error: accessing member 'M' requires an instance ex
 ResolutionErrors.dfy(63,7): Error: unresolved identifier: N

 ResolutionErrors.dfy(66,8): Error: non-function expression (of type int) is called with parameters

 ResolutionErrors.dfy(67,14): Error: member 'z' does not exist in type 'Global'

-ResolutionErrors.dfy(260,4): Error: label shadows an enclosing label

-ResolutionErrors.dfy(265,2): Error: duplicate label

-ResolutionErrors.dfy(291,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

-ResolutionErrors.dfy(292,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

-ResolutionErrors.dfy(294,9): Error: a constructor is allowed to be called only when an object is being allocated

-ResolutionErrors.dfy(308,16): Error: arguments must have the same type (got int and DTD_List)

-ResolutionErrors.dfy(309,16): Error: arguments must have the same type (got DTD_List and int)

-ResolutionErrors.dfy(310,25): Error: arguments must have the same type (got bool and int)

-ResolutionErrors.dfy(322,15): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(347,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)

-ResolutionErrors.dfy(359,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)

-ResolutionErrors.dfy(367,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)

-ResolutionErrors.dfy(372,6): Error: all lines in a calculation must have the same type (got int after bool)

-ResolutionErrors.dfy(375,6): Error: first argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(375,6): Error: second argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(376,10): Error: first argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(376,10): Error: second argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(381,10): Error: first argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(381,10): Error: second argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(470,7): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(476,2): Error: non-ghost variable cannot be assigned a value that depends on a ghost

-ResolutionErrors.dfy(549,18): Error: unresolved identifier: w

-ResolutionErrors.dfy(656,11): Error: lemmas are not allowed to have modifies clauses

-ResolutionErrors.dfy(918,9): Error: unresolved identifier: s

-ResolutionErrors.dfy(929,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))

-ResolutionErrors.dfy(930,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))

-ResolutionErrors.dfy(936,16): Error: condition is expected to be of type bool, but is int

-ResolutionErrors.dfy(937,16): Error: member 3 does not exist in datatype _tuple#3

-ResolutionErrors.dfy(937,26): Error: member x does not exist in datatype _tuple#2

-ResolutionErrors.dfy(960,15): Error: arguments to / must have the same type (got real and int)

-ResolutionErrors.dfy(961,10): Error: second argument to % must be of type int (instead got real)

-ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait

-ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)

-ResolutionErrors.dfy(1134,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

-ResolutionErrors.dfy(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

+ResolutionErrors.dfy(311,4): Error: label shadows an enclosing label

+ResolutionErrors.dfy(316,2): Error: duplicate label

+ResolutionErrors.dfy(342,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

+ResolutionErrors.dfy(343,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

+ResolutionErrors.dfy(345,9): Error: a constructor is allowed to be called only when an object is being allocated

+ResolutionErrors.dfy(359,16): Error: arguments must have the same type (got int and DTD_List)

+ResolutionErrors.dfy(360,16): Error: arguments must have the same type (got DTD_List and int)

+ResolutionErrors.dfy(361,25): Error: arguments must have the same type (got bool and int)

+ResolutionErrors.dfy(375,15): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(400,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)

+ResolutionErrors.dfy(412,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)

+ResolutionErrors.dfy(420,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)

+ResolutionErrors.dfy(425,6): Error: all lines in a calculation must have the same type (got int after bool)

+ResolutionErrors.dfy(428,6): Error: first argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(428,6): Error: second argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(429,10): Error: first argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(429,10): Error: second argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(434,10): Error: first argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(434,10): Error: second argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(526,7): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(532,2): Error: non-ghost variable cannot be assigned a value that depends on a ghost

+ResolutionErrors.dfy(603,18): Error: unresolved identifier: w

+ResolutionErrors.dfy(714,11): Error: lemmas are not allowed to have modifies clauses

+ResolutionErrors.dfy(976,9): Error: unresolved identifier: s

+ResolutionErrors.dfy(987,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))

+ResolutionErrors.dfy(988,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))

+ResolutionErrors.dfy(994,16): Error: condition is expected to be of type bool, but is int

+ResolutionErrors.dfy(995,16): Error: member 3 does not exist in datatype _tuple#3

+ResolutionErrors.dfy(995,26): Error: member x does not exist in datatype _tuple#2

+ResolutionErrors.dfy(1018,15): Error: arguments to / must have the same type (got real and int)

+ResolutionErrors.dfy(1019,10): Error: second argument to % must be of type int (instead got real)

+ResolutionErrors.dfy(1164,8): Error: new cannot be applied to a trait

+ResolutionErrors.dfy(1185,13): Error: first argument to / must be of numeric type (instead got set<bool>)

+ResolutionErrors.dfy(1192,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

+ResolutionErrors.dfy(1207,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

 193 resolution/type errors detected in ResolutionErrors.dfy