Set up the same test infrastructure as in Boogie.

1 files changed, 135 insertions, 0 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
new file mode 100644
index 00000000..eb9b244b
--- /dev/null
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -0,0 +1,135 @@
+ResolutionErrors.dfy(499,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

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

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

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

+ResolutionErrors.dfy(565,18): Error: type of bound variable 'z' could not determined; please specify the type explicitly

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

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

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

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

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

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

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

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

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

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

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

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

+ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.

+ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.

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

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

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

+ResolutionErrors.dfy(700,16): 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(700,16): Error: a hint is not allowed to update heap locations

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

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

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

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

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

+ResolutionErrors.dfy(732,16): 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(732,16): Error: a hint is not allowed to update heap locations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+ResolutionErrors.dfy(429,2): Error: More than one default constructor

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

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

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

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

+ResolutionErrors.dfy(117,9): Error: actual out-parameter 0 is required to be a ghost variable

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

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

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

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

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

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

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

+ResolutionErrors.dfy(196,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure

+ResolutionErrors.dfy(219,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

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

+ResolutionErrors.dfy(235,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

+ResolutionErrors.dfy(240,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)

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

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

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

+ResolutionErrors.dfy(443,9): Error: class Lamb does not have a default constructor

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

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

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

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

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

+ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as frame targets (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>)

+ResolutionErrors.dfy(26,11): Error: array selection requires an array4 (got array<T>)

+ResolutionErrors.dfy(56,14): Error: a field must be selected via an object, not just a class name

+ResolutionErrors.dfy(57,7): Error: unresolved identifier: F

+ResolutionErrors.dfy(58,14): Error: an instance function must be selected via an object, not just a class name

+ResolutionErrors.dfy(58,7): Error: call to instance function requires an instance

+ResolutionErrors.dfy(59,7): Error: unresolved identifier: G

+ResolutionErrors.dfy(61,7): Error: unresolved identifier: M

+ResolutionErrors.dfy(62,7): Error: call to instance method requires an instance

+ResolutionErrors.dfy(63,7): Error: unresolved identifier: N

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

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

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

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

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

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

+ResolutionErrors.dfy(96,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)

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

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

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

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

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

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

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

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

+ResolutionErrors.dfy(311,18): Error: ghost fields are allowed only in specification contexts

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

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

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

+ResolutionErrors.dfy(365,6): Error: arguments to + must be int or real or a collection type (instead got bool)

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

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

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

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

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

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

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

+ResolutionErrors.dfy(384,6): 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(406,6): Error: calls to methods with side-effects are not allowed inside a hint

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

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

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

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

+ResolutionErrors.dfy(541,7): Error: let-such-that expressions are allowed only in ghost contexts

+ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts

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

+ResolutionErrors.dfy(545,7): Error: let-such-that expressions are allowed only in ghost contexts

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

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

+134 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\ResolutionErrors.dfy