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/dafny1/SeparationLogicList.dfy | |
| 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/dafny1/SeparationLogicList.dfy')
| -rw-r--r-- | Test/dafny1/SeparationLogicList.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
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
|