Added back in various ghost tests

1 files changed, 8 insertions, 1 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 55d2e79c..0286778b 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -125,6 +125,10 @@ ResolutionErrors.dfy(142,35): Error: ghost variables are allowed only in specifi
 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(231,12): Error: trying to break out of more loop levels than there are enclosing loops

+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(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

@@ -164,6 +168,7 @@ ResolutionErrors.dfy(345,9): Error: a constructor is allowed to be called only w
 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(367,14): Error: ghost fields are allowed only in specification contexts

 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>)

@@ -175,9 +180,11 @@ ResolutionErrors.dfy(429,10): Error: first argument to ==> must be of type bool
 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(442,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(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(608,24): Error: ghost variables are allowed only in specification contexts

 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))

@@ -191,4 +198,4 @@ 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

+200 resolution/type errors detected in ResolutionErrors.dfy