diff options
| author |  leino <unknown> | 2015-09-20 21:51:42 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-09-20 21:51:42 -0700 |
| commit | 800885b4d7d0164803c0c2f117b78c65479283f9 (patch) | |
| tree | d5ffd8318ffeed8fa300a9e872461f38455c28ed /Test/dafny0/ParallelResolveErrors.dfy.expect | |
| parent | b9319e38746bc6a2043cb7c979c4ccd4b175b86c (diff) | |
Preliminary refactoring of ghost-statement computations to after type checking
Diffstat (limited to 'Test/dafny0/ParallelResolveErrors.dfy.expect')
| -rw-r--r-- | Test/dafny0/ParallelResolveErrors.dfy.expect | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Test/dafny0/ParallelResolveErrors.dfy.expect b/Test/dafny0/ParallelResolveErrors.dfy.expect index 7305bfce..00030994 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy.expect +++ b/Test/dafny0/ParallelResolveErrors.dfy.expect @@ -1,7 +1,8 @@ ParallelResolveErrors.dfy(10,9): 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)
ParallelResolveErrors.dfy(21,4): Error: LHS of assignment must denote a mutable variable
ParallelResolveErrors.dfy(26,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
-ParallelResolveErrors.dfy(44,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ParallelResolveErrors.dfy(43,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
+ParallelResolveErrors.dfy(44,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
ParallelResolveErrors.dfy(56,13): Error: new allocation not supported in forall statements
ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost context
ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context
@@ -19,4 +20,4 @@ ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scop ParallelResolveErrors.dfy(107,9): Error: the body of the enclosing forall statement is not allowed to update heap locations
ParallelResolveErrors.dfy(115,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
ParallelResolveErrors.dfy(120,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
-21 resolution/type errors detected in ParallelResolveErrors.dfy
+22 resolution/type errors detected in ParallelResolveErrors.dfy
|