diff options
| author |  Rustan Leino <unknown> | 2013-02-13 18:11:11 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-02-13 18:11:11 -0800 |
| commit | b0e4b4eaee0e98e04b4b7254f2f09540f2d7b904 (patch) | |
| tree | 85be5860d4e513ecbcc76661411b077bb3fb5021 /Test | |
| parent | 2c74f9200db870814ea3dae63484cbe969ec3526 (diff) | |
Frame expressions are now checked to be well formed.
(A nice consequence of this is that the method IsTotal is no longer needed.)
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 5 | ||||
| -rw-r--r-- | Test/dafny0/Definedness.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny1/BinaryTree.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny1/SeparationLogicList.dfy | 2 |
4 files changed, 7 insertions, 4 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index ddabad3d..f2fccb73 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -318,6 +318,9 @@ Execution trace: Definedness.dfy(33,16): Error: target object may be null
Execution trace:
(0,0): anon0
+Definedness.dfy(42,16): Error: target object may be null
+Execution trace:
+ (0,0): anon0
Definedness.dfy(50,18): Error: target object may be null
Execution trace:
(0,0): anon0
@@ -473,7 +476,7 @@ Execution trace: (0,0): anon2
(0,0): anon8_Else
-Dafny program verifier finished with 22 verified, 36 errors
+Dafny program verifier finished with 21 verified, 37 errors
-------------------- FunctionSpecifications.dfy --------------------
FunctionSpecifications.dfy(32,3): Error BP5003: A postcondition might not hold on this return path.
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;
}
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
|