Frame expressions are now checked to be well formed.

(A nice consequence of this is that the method IsTotal is no longer needed.)

1 files changed, 1 insertions, 1 deletions

diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index f99d1503..58337a26 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -39,7 +39,7 @@ class SoWellformed {
   }

 

   method O(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

-    modifies a.next;  // this may not be well-defined, but that's okay for modifies clauses

+    modifies a.next;  // error: this is not well-defined if a == null (but it's okay to have a.next==null)

   {

     c := true;

   }