diff options
| author |  stefanheule <unknown> | 2012-09-28 09:50:14 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-09-28 09:50:14 +0200 |
| commit | 35d2a968b3fe15ca88c5b8dcf6047da434ab6ce2 (patch) | |
| tree | d66da1ee253a27edf90366e74588c6cff78c8729 /Chalice | |
| parent | 536ba466d072e688c002b461a4b2ceebbd4f4c44 (diff) | |
Chalice: Add a test-case for a recently fixed issue.
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/tests/general-tests/ll-lastnode.chalice | 82 | ||||
| -rw-r--r-- | Chalice/tests/general-tests/ll-lastnode.output.txt | 6 |
2 files changed, 88 insertions, 0 deletions
diff --git a/Chalice/tests/general-tests/ll-lastnode.chalice b/Chalice/tests/general-tests/ll-lastnode.chalice new file mode 100644 index 00000000..f7a44cfe --- /dev/null +++ b/Chalice/tests/general-tests/ll-lastnode.chalice @@ -0,0 +1,82 @@ +// This test case showed a triggering problem (and potentially a matching loop).
+// The quantified assertion and postcondition that did not verify are highlighted below.
+class Node
+{
+ var val:int
+ var next:Node
+ var break_here:bool
+
+ predicate lseg
+ {
+ acc(break_here) && (!break_here ==> acc(val) && acc(next) && (next!=null ==> next.lseg))
+ }
+
+ predicate xlseg
+ {
+ acc(val) && acc(next) && (next!=null ==> next.lseg)
+ }
+
+ function length():int
+ requires lseg
+ ensures 0 <= result
+ {
+ unfolding lseg in (break_here ? 0 : (next==null ? 1 : 1+next.length()))
+ }
+
+ function xlength():int
+ requires xlseg
+ ensures 0 < result
+ {
+ unfolding xlseg in (next==null ? 1 : 1+next.length())
+ }
+
+ function get(i:int):int
+ requires lseg && i>=0 && i<length()
+ {
+ unfolding lseg in i==0 ? val : next.get(i-1)
+ }
+
+ function xget(i:int):int
+ requires xlseg && i>=0 && i<xlength()
+ {
+ unfolding xlseg in i==0 ? val : next.get(i-1)
+ }
+
+ function get_next_seg():Node
+ requires lseg
+ {
+ unfolding lseg in break_here ? this : (next==null ? next : next.get_next_seg())
+ }
+
+ method lastNode() returns(res:Node)
+ requires lseg && length()>0
+ ensures res != null && lseg && res.xlseg
+ ensures res.xlength()==1 && res.xget(0)==old(get(length()-1))
+ ensures length() == old(length()-1)
+ // Did not verify.
+ ensures (forall i:int :: 0<=i && i<length() ==> get(i) == old(get(i)))
+ {
+ var I:int
+ var h:Node
+
+ res:=this
+ unfold lseg
+ break_here:=true
+ fold lseg
+ fold xlseg
+
+ while(res.xlength()>1)
+ invariant res!=null && lseg && res.xlseg &&
+ res==get_next_seg() && // new invariant
+ length() + res.xlength() == old(length()) &&
+ 0 <= length() && length() < old(length()) &&
+ (forall i:int :: 0<=i && i<length() ==> get(i)==old(get(i))) &&
+ (forall i:int :: length()<=i && i<old(length()) ==> res.xget(i-length())==old(get(i)))
+ {
+ // We are not interested (at the moment) in verifying the loop.
+ assume false
+ }
+ // Did not verify.
+ assert (forall i:int :: length()<=i && i<old(length()) ==> res.xget(i-length())==old(get(i)))
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/general-tests/ll-lastnode.output.txt b/Chalice/tests/general-tests/ll-lastnode.output.txt new file mode 100644 index 00000000..a02dd2d8 --- /dev/null +++ b/Chalice/tests/general-tests/ll-lastnode.output.txt @@ -0,0 +1,6 @@ +Verification of ll-lastnode.chalice using parameters=""
+
+ + 77.9: Assumption introduces a contradiction. + +Boogie program verifier finished with 0 errors and 1 smoke test warnings
|