move: Split ResolutionErrors.dfy into 10 smaller files (#5137)

This PR just moves the lines of the previous
`dafny0/ResolutionErrors.dfy` test file into 10 smaller files. In some
files, the `--allow-axioms` flag was dropped, because it was not needed.

This PR paves the way to changing these tests to be run with both the
old and the new resolver.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors0.dfy.expect

@@ -0,0 +1,70 @@
+ResolutionErrors0.dfy(323,33): Warning: constructors no longer need 'this' to be listed in modifies clauses
+ResolutionErrors0.dfy(13,18): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors0.dfy(25,13): Error: array selection requires an array2 (got array3<T>)
+ResolutionErrors0.dfy(27,13): Error: array selection requires an array4 (got array<T>)
+ResolutionErrors0.dfy(26,14): Error: element selection requires a sequence, array, multiset, or map (got array3<T>)
+ResolutionErrors0.dfy(57,16): Error: accessing member 'X' requires an instance expression
+ResolutionErrors0.dfy(58,9): Error: unresolved identifier: F
+ResolutionErrors0.dfy(59,16): Error: accessing member 'F' requires an instance expression
+ResolutionErrors0.dfy(60,9): Error: unresolved identifier: G
+ResolutionErrors0.dfy(62,9): Error: unresolved identifier: M
+ResolutionErrors0.dfy(63,16): Error: accessing member 'M' requires an instance expression
+ResolutionErrors0.dfy(64,9): Error: unresolved identifier: N
+ResolutionErrors0.dfy(67,10): Error: non-function expression (of type int) is called with parameters
+ResolutionErrors0.dfy(68,16): Error: member 'z' does not exist in non-null type 'Global'
+ResolutionErrors0.dfy(51,15): Error: 'this' is not allowed in a 'static' context
+ResolutionErrors0.dfy(88,16): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
+ResolutionErrors0.dfy(93,16): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors0.dfy(94,16): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors0.dfy(96,16): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors0.dfy(98,20): Error: wrong number of arguments (got 2, but datatype constructor 'David' expects 1: (x: int))
+ResolutionErrors0.dfy(116,11): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization.
+ResolutionErrors0.dfy(117,11): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
+ResolutionErrors0.dfy(121,13): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization.
+ResolutionErrors0.dfy(122,12): Error: actual out-parameter is required to be a ghost variable
+ResolutionErrors0.dfy(129,17): Error: ghost variables such as gg are allowed only in specification contexts. gg was inferred to be ghost based on its declaration or initialization.
+ResolutionErrors0.dfy(133,25): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization.
+ResolutionErrors0.dfy(140,6): Error: ghost variables such as y are allowed only in specification contexts. y was inferred to be ghost based on its declaration or initialization.
+ResolutionErrors0.dfy(144,23): Error: ghost variables such as gg are allowed only in specification contexts. gg was inferred to be ghost based on its declaration or initialization.
+ResolutionErrors0.dfy(145,37): Error: ghost variables such as gg are allowed only in specification contexts. gg was inferred to be ghost based on its declaration or initialization.
+ResolutionErrors0.dfy(154,12): Error: only ghost methods can be called from this context
+ResolutionErrors0.dfy(244,29): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors0.dfy(267,14): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors0.dfy(281,14): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors0.dfy(286,10): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
+ResolutionErrors0.dfy(306,12): Error: label shadows an enclosing label
+ResolutionErrors0.dfy(311,10): Error: duplicate label
+ResolutionErrors0.dfy(313,10): Error: label shadows a dominating label
+ResolutionErrors0.dfy(329,11): Error: a constructor is allowed to be called only when an object is being allocated
+ResolutionErrors0.dfy(345,27): Error: arguments must have comparable types (got bool and int)
+ResolutionErrors0.dfy(343,18): Error: arguments must have comparable types (got int and DTD_List)
+ResolutionErrors0.dfy(344,18): Error: arguments must have comparable types (got DTD_List and int)
+ResolutionErrors0.dfy(358,17): Error: ghost variables such as b are allowed only in specification contexts. b was inferred to be ghost based on its declaration or initialization.
+ResolutionErrors0.dfy(382,7): Error: incorrect argument type at index 1 for method in-parameter 'b' (expected GenericClass<int>, found GenericClass<bool>) (non-variant type parameter would require int = bool)
+ResolutionErrors0.dfy(396,13): Error: incorrect argument type at index 0 for datatype constructor parameter 'hd' (expected _T0, found int)
+ResolutionErrors0.dfy(397,9): Error: incorrect argument type at index 0 for datatype constructor parameter 'hd' (expected _T0, found int)
+ResolutionErrors0.dfy(406,8): Error: all lines in a calculation must have the same type (got int after bool)
+ResolutionErrors0.dfy(410,8): Error: all lines in a calculation must have the same type (got int after bool)
+ResolutionErrors0.dfy(413,8): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors0.dfy(413,8): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors0.dfy(414,12): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors0.dfy(414,12): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors0.dfy(415,12): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors0.dfy(415,12): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors0.dfy(413,8): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors0.dfy(413,8): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors0.dfy(419,12): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors0.dfy(419,12): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors0.dfy(418,8): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors0.dfy(418,8): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors0.dfy(405,8): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
+ResolutionErrors0.dfy(405,8): Error: arguments must have comparable types (got bool and int)
+ResolutionErrors0.dfy(405,8): Error: arguments must have comparable types (got bool and int)
+ResolutionErrors0.dfy(409,8): Error: arguments must have comparable types (got bool and int)
+ResolutionErrors0.dfy(409,8): Error: arguments must have comparable types (got bool and int)
+ResolutionErrors0.dfy(443,13): Error: in a hint, calls are allowed only to lemmas
+ResolutionErrors0.dfy(445,10): Error: a hint is not allowed to make heap updates
+ResolutionErrors0.dfy(447,10): Error: a hint is not allowed to update a variable it doesn't declare
+ResolutionErrors0.dfy(468,4): Error: More than one anonymous constructor
+ResolutionErrors0.dfy(481,15): Error: class Lamb does not have an anonymous constructor
+68 resolution/type errors detected in ResolutionErrors0.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors1.dfy

@@ -0,0 +1,182 @@
+// RUN: %exits-with 2 %verify --allow-axioms "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// ------------------------ inferred type arguments ----------------------------
+
+// Put the following tests in a separate module, so that the method bodies will
+// be type checked even if there are resolution errors in other modules.
+
+module NoTypeArgs0 {
+ datatype List<+T> = Nil | Cons(T, List)
+ datatype Tree<+A,+B> = Leaf(A, B) | Node(Tree, Tree<B,A>)
+
+ method DoAPrefix0<A, B, C>(xs: List) returns (ys: List<A>)
+ {
+ ys := xs;
+ }
+
+ method DoAPrefix1<A, B, C>(xs: List) returns (ys: List<B>)
+ {
+ ys := xs; // error: List<B> cannot be assign to a List<A>
+ }
+
+ method DoAPrefix2<A, B, C>(xs: List) returns (ys: List<B>)
+ {
+ ys := xs; // error: List<B> cannot be assign to a List<A>
+ }
+
+ ghost function FTree0(t: Tree): Tree
+ {
+ match t
+ case Leaf(_,_) => t
+ case Node(x, y) => x
+ }
+
+ ghost function FTree1(t: Tree): Tree
+ {
+ match t
+ case Leaf(_,_) => t
+ case Node(x, y) => y // error: y does not have the right type
+ }
+
+ ghost function FTree2<A,B,C>(t: Tree): Tree<A,B>
+ {
+ t
+ }
+}
+
+module NoTypeArgs1 {
+ datatype Tree<A,B> = Leaf(A, B) | Node(Tree, Tree<B,A>)
+
+ ghost function FTree3<T>(t: Tree): Tree<T,T> // error: type of 't' does not have enough type parameters
+ {
+ t
+ }
+}
+
+// ----------- let-such-that expressions ------------------------
+
+module MiscMisc {
+ 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)
+
+ 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;
+ }
+}
+
+// ------------ quantified variables whose types are not inferred ----------
+
+module NonInferredType {
+ ghost predicate P<T>(x: T)
+
+ method InferredType(x: int)
+ {
+ var t;
+ assume forall z :: P(z) && z == t;
+ assume t == x; // this statement determines the type of t and z
+ }
+
+ method NonInferredType(x: int)
+ {
+ var t; // error: the type of t is not determined
+ assume forall z :: P(z) && z == t; // error: the type of z is not determined
+ }
+}
+
+// ------------ Here are some tests that lemma contexts don't allocate objects -------------
+
+module GhostAllocationTests {
+ class G { }
+ iterator GIter() { }
+ class H { constructor () }
+ lemma GhostNew0()
+ ensures exists o: G :: fresh(o)
+ {
+ var p := new G; // error: lemma context is not allowed to allocate state
+ p := new G; // error: ditto
+ }
+
+ method GhostNew1(n: nat, ghost g: int) returns (t: G, z: int)
+ {
+ if n < 0 {
+ z, t := 5, new G; // fine
+ }
+ if n < g {
+ var tt := new H(); // error: 'new' not allowed in ghost contexts
+ }
+ }
+
+ method GhostNew2(ghost b: bool)
+ {
+ if (b) {
+ var y := new GIter(); // error: 'new' not allowed in ghost contexts (and a non-ghost method is not allowed to be called here either)
+ }
+ }
+}
+module MoreGhostAllocationTests {
+ class G { }
+ method GhostNew3(n: nat) {
+ var g := new G;
+ calc {
+ 5;
+ { var y := new G; } // error: 'new' not allowed in lemma contexts
+ 2 + 3;
+ }
+ }
+ ghost method GhostNew4(g: G)
+ modifies g
+ {
+ }
+}
+
+module NewForallAssign {
+ class G { }
+ method NewForallTest(n: nat) {
+ var a := new G[n];
+ forall i | 0 <= i < n {
+ a[i] := new G; // error: 'new' is currently not supported in forall statements
+ } }
+}
+module NewForallProof {
+ class G { }
+ method NewForallTest(n: nat) { var a := new G[n];
+ forall i | 0 <= i < n ensures true { // this makes the whole 'forall' statement into a ghost statement
+ a[i] := new G; // error: proof-forall cannot update state (and 'new' not allowed in ghost contexts, but that's checked at a later stage)
+ } }
+}
+
+// ------------------------- underspecified types ------------------------------
+
+module UnderspecifiedTypes {
+ method M(S: set<int>) {
+ var n, p, T0 :| 12 <= n && n in T0 && 10 <= p && p in T0 && T0 <= S && p % 2 != n % 2;
+ var T1 :| 12 in T1 && T1 <= S;
+ var T2 :| T2 <= S && 12 in T2;
+ var T3 :| 120 in T3; // error: underspecified type
+ var T3'0: set<int> :| 120 in T3'0;
+ var T3'1: multiset<int> :| 120 in T3'1;
+ var T3'2: map<int,bool> :| 120 in T3'2;
+ var T3'3: seq<int> :| 120 in T3'3;
+ var T3'4: bool :| 120 in T3'4; // error: second argument to 'in' cannot be bool
+ var T4 :| T4 <= S;
+ }
+}
+
+// ------------------------- lemmas ------------------------------
+
+module MiscLemma {
+ class L { }
+
+ // a lemma is allowed to have out-parameters, but not a modifies clause
+ lemma MyLemma(x: int, l: L) returns (y: int)
+ requires 0 <= x
+ modifies l
+ ensures 0 <= y
+ {
+ y := x;
+ }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors1.dfy.expect

@@ -0,0 +1,21 @@
+ResolutionErrors1.dfy(20,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>) (covariant type parameter would require A <: B)
+ResolutionErrors1.dfy(25,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>) (covariant type parameter would require A <: B)
+ResolutionErrors1.dfy(39,23): Error: type of case bodies do not agree (found Tree<_T1, _T0>, previous types Tree<_T0, _T1>) (covariant type parameter 0 would require _T1 <: _T0)
+ResolutionErrors1.dfy(51,30): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree
+ResolutionErrors1.dfy(66,20): Error: unresolved identifier: w
+ResolutionErrors1.dfy(85,8): Error: the type of this local variable is underspecified
+ResolutionErrors1.dfy(86,25): Error: the type of this variable is underspecified
+ResolutionErrors1.dfy(86,23): Error: type parameter 'T' (inferred to be '?') in the function call to 'P' could not be determined
+ResolutionErrors1.dfy(86,18): Error: type of bound variable 'z' could not be determined; please specify the type explicitly
+ResolutionErrors1.dfy(99,13): Error: a lemma is not allowed to use 'new'
+ResolutionErrors1.dfy(100,9): Error: a lemma is not allowed to use 'new'
+ResolutionErrors1.dfy(109,16): Error: only ghost methods can be called from this context
+ResolutionErrors1.dfy(116,15): Error: only ghost methods can be called from this context
+ResolutionErrors1.dfy(126,17): Error: a hint is not allowed to use 'new'
+ResolutionErrors1.dfy(141,14): Error: new allocation not supported in aggregate assignments
+ResolutionErrors1.dfy(148,14): Error: a forall statement is not allowed to use 'new'
+ResolutionErrors1.dfy(148,11): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression
+ResolutionErrors1.dfy(164,26): Error: second argument to "in" must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got bool)
+ResolutionErrors1.dfy(159,18): Error: second argument to "in" must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got ?)
+ResolutionErrors1.dfy(177,13): Error: lemmas are not allowed to have modifies clauses
+20 resolution/type errors detected in ResolutionErrors1.dfy