diff options
| author |  leino <unknown> | 2014-12-02 19:41:39 -0800 |
|---|---|---|
| committer | leino <unknown> | 2014-12-02 19:41:39 -0800 |
| commit | 3d8fd4cc56db82eb5c83f1e2061e88859f40778d (patch) | |
| tree | dca65a6090582985c9c0cec2fdbc0aae5164dd9f /Test/dafny0/RefinementModificationChecking.dfy.expect | |
| parent | 5bb3834b184f7f2a2f9d3d5b1d8acf2de6b3b8fc (diff) | |
Fixed some issues with assignments in refinements, both soundness bugs in previous version and changes necessitated by recent parsing refactoring
Diffstat (limited to 'Test/dafny0/RefinementModificationChecking.dfy.expect')
| -rw-r--r-- | Test/dafny0/RefinementModificationChecking.dfy.expect | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/Test/dafny0/RefinementModificationChecking.dfy.expect b/Test/dafny0/RefinementModificationChecking.dfy.expect index 060ee3e4..675d244e 100644 --- a/Test/dafny0/RefinementModificationChecking.dfy.expect +++ b/Test/dafny0/RefinementModificationChecking.dfy.expect @@ -1,3 +1,6 @@ -RefinementModificationChecking.dfy(19,4): Error: cannot assign to variable defined previously
-RefinementModificationChecking.dfy(20,4): Error: cannot assign to variable defined previously
-2 resolution/type errors detected in RefinementModificationChecking.dfy
+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)
+5 resolution/type errors detected in RefinementModificationChecking.dfy
|