Skip to content

Commit

Permalink
Added a test case for Silicon
Browse files Browse the repository at this point in the history
  • Loading branch information
mschwerhoff committed Jan 6, 2014
1 parent 2341c03 commit 96236a5
Showing 1 changed file with 20 additions and 0 deletions.
20 changes: 20 additions & 0 deletions src/test/resources/all/issues/silicon/0053.sil
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
var next: Ref
var val: Int

predicate valid(this: Ref) {
acc(this.next) && acc(this.val) &&
(this.next != null ==> acc(valid(this.next)))
}

method traverse(list: Ref)
requires acc(valid(list))
{
var tmp: Ref := list

while (tmp != null)
invariant (tmp != null) ==> acc(valid(tmp))
{
unfold acc(valid(tmp))
tmp := tmp.next
}
}

0 comments on commit 96236a5

Please sign in to comment.