diff options
Diffstat (limited to 'Test/dafny0/RefinementModificationChecking.dfy.expect')
| -rw-r--r-- | Test/dafny0/RefinementModificationChecking.dfy.expect | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Test/dafny0/RefinementModificationChecking.dfy.expect b/Test/dafny0/RefinementModificationChecking.dfy.expect index 675d244e..1a5df922 100644 --- a/Test/dafny0/RefinementModificationChecking.dfy.expect +++ b/Test/dafny0/RefinementModificationChecking.dfy.expect @@ -1,6 +1,6 @@ -RefinementModificationChecking.dfy(19,4): Error: refinement method cannot assign to variable defined in parent module ('t')
-RefinementModificationChecking.dfy(20,4): Error: refinement method cannot assign to variable defined in parent module ('r')
-RefinementModificationChecking.dfy(21,4): Error: refinement method cannot assign to a field defined in parent module ('f')
-RefinementModificationChecking.dfy(47,15): Error: assignment RHS in refinement method is not allowed to affect previously defined state
-RefinementModificationChecking.dfy(49,11): Error: new assignments in a refinement method can only assign to state that the module defines (which never includes array elements)
+RefinementModificationChecking.dfy(22,6): Error: refinement method cannot assign to variable defined in parent module ('t')
+RefinementModificationChecking.dfy(23,6): Error: refinement method cannot assign to variable defined in parent module ('r')
+RefinementModificationChecking.dfy(24,6): Error: refinement method cannot assign to a field defined in parent module ('f')
+RefinementModificationChecking.dfy(51,15): Error: assignment RHS in refinement method is not allowed to affect previously defined state
+RefinementModificationChecking.dfy(53,11): Error: new assignments in a refinement method can only assign to state that the module defines (which never includes array elements)
5 resolution/type errors detected in RefinementModificationChecking.dfy
|