Preliminary refactoring of ghost-statement computations to after type checking

1 files changed, 2 insertions, 11 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index b5c93ac1..8debdbf9 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -21,14 +21,12 @@ ResolutionErrors.dfy(642,21): Error: the type of this variable is underspecified
 ResolutionErrors.dfy(680,13): Error: calls to methods with side-effects are not allowed inside a hint

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

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

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

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

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

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

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

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

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

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

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

@@ -126,11 +124,7 @@ 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(198,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure

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

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

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

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

 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

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

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

@@ -182,10 +175,8 @@ ResolutionErrors.dfy(376,10): Error: first argument to ==> must be of type bool
 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(386,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(470,7): Error: ghost variables are allowed only in specification contexts

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

-ResolutionErrors.dfy(546,20): 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

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

-202 resolution/type errors detected in ResolutionErrors.dfy

+193 resolution/type errors detected in ResolutionErrors.dfy