From b0e4b4eaee0e98e04b4b7254f2f09540f2d7b904 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Wed, 13 Feb 2013 18:11:11 -0800
Subject: Frame expressions are now checked to be well formed. (A nice
 consequence of this is that the method IsTotal is no longer needed.)

---
 Test/dafny1/BinaryTree.dfy          | 2 +-
 Test/dafny1/SeparationLogicList.dfy | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'Test/dafny1')

diff --git a/Test/dafny1/BinaryTree.dfy b/Test/dafny1/BinaryTree.dfy
index 88b06605..ea915f69 100644
--- a/Test/dafny1/BinaryTree.dfy
+++ b/Test/dafny1/BinaryTree.dfy
@@ -50,7 +50,7 @@ class IntSet {
 
   static method InsertHelper(x: int, n: Node) returns (m: Node)
     requires n == null || n.Valid();
-    modifies n.Repr;
+    modifies if n != null then n.Repr else {};
     ensures m != null && m.Valid();
     ensures n == null ==> fresh(m.Repr) && m.Contents == {x};
     ensures n != null ==> m == n && n.Contents == old(n.Contents) + {x};
diff --git a/Test/dafny1/SeparationLogicList.dfy b/Test/dafny1/SeparationLogicList.dfy
index 56a64bd6..0b803afc 100644
--- a/Test/dafny1/SeparationLogicList.dfy
+++ b/Test/dafny1/SeparationLogicList.dfy
@@ -53,7 +53,7 @@ class ListNode<T> {
   var next: ListNode<T>;
 
   static function IsList(l: ListNode<T>): bool
-    reads l, l.Repr;
+    reads l, if l != null then l.Repr else {};
   {
     if l == null then
       true
-- 
cgit v1.2.3