diff options
Diffstat (limited to 'Test/dafny1')
| -rw-r--r-- | Test/dafny1/BinaryTree.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny1/SeparationLogicList.dfy | 2 |
2 files changed, 2 insertions, 2 deletions
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
|