diff options
Diffstat (limited to 'Chalice/tests/predicates')
22 files changed, 252 insertions, 23 deletions
diff --git a/Chalice/tests/predicates/FoldUnfoldExperiments.output.txt b/Chalice/tests/predicates/FoldUnfoldExperiments.output.txt index 7239cf05..ba48d6f4 100644 --- a/Chalice/tests/predicates/FoldUnfoldExperiments.output.txt +++ b/Chalice/tests/predicates/FoldUnfoldExperiments.output.txt @@ -1,4 +1,4 @@ Verification of FoldUnfoldExperiments.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/LinkedList-various.chalice b/Chalice/tests/predicates/LinkedList-various.chalice new file mode 100644 index 00000000..a888b647 --- /dev/null +++ b/Chalice/tests/predicates/LinkedList-various.chalice @@ -0,0 +1,176 @@ +class Node
+{
+ var v:int;
+ var n:Node;
+
+ predicate inv
+ { acc(v) && acc(n) && (n!=null ==> n.inv) }
+
+ function len():int
+ requires inv;
+ ensures result>0;
+ {
+ unfolding inv in (n==null) ? 1 : 1+n.len()
+ }
+
+ function get(i:int):int
+ requires inv && 0<=i && i<len();
+ {
+ unfolding inv in (i==0) ? v : n.get(i-1)
+ }
+
+ method addLast(x:int)
+ requires inv;
+ ensures inv;
+ ensures len()==old(len())+1 && get(old(len()))==x;
+ ensures (forall i:int :: 0<=i && i<old(len()) ==> get(i)==old(get(i)));
+ {
+ unfold inv;
+ if(n==null)
+ {
+ n:=new Node;
+ n.v:=x; n.n:=null;
+ fold n.inv;
+ }
+ else
+ {
+ call n.addLast(x);
+ }
+ fold inv;
+ }
+
+ method append(p:List)
+ requires inv && p!=null && p.inv;
+ ensures inv;
+ ensures len()==old(len()+p.len());
+ ensures (forall i in [0..old(len())] :: get(i)==old(get(i)));
+ ensures (forall i in [old(len())..len()] :: get(i)==old(p.get(i-len())));
+ {
+ unfold inv;
+ if(n==null)
+ {
+ unfold p.inv;
+ n:=p.c;
+ }
+ else
+ {
+ call n.append(p);
+ }
+ fold inv;
+ }
+
+ method remove(i:int)
+ requires inv && i>=0 && i<len()-1;
+ ensures inv;
+ ensures len()==old(len())-1;
+ ensures (forall j in [0..i+1] :: get(j)==old(get(j)));
+ ensures (forall j in [i+1..len()] :: get(j)==old(get(j+1)));
+ {
+ unfold inv;
+ if(i==0)
+ {
+ unfold n.inv;
+ n:=n.n;
+ }
+ else
+ {
+ call n.remove(i-1);
+ }
+ fold inv;
+ }
+}
+
+class List
+{
+ var c:Node;
+
+ predicate inv { acc(c) && (c!=null ==> c.inv) }
+
+ function len():int
+ requires inv;
+ ensures result>=0;
+ {
+ unfolding inv in (c==null) ? 0 : c.len()
+ }
+
+ function get(i:int):int
+ requires inv && 0<=i && i<len();
+ {
+ unfolding inv in c.get(i)
+ }
+
+ method addFirst(x:int)
+ requires inv;
+ ensures inv;
+ ensures len()==old(len())+1 && get(0)==x;
+ ensures (forall i:int :: 1<=i && i<len() ==> get(i)==old(get(i-1)));
+ {
+ var p:Node;
+
+ unfold inv;
+ p:=new Node; p.v:=x; p.n:=c; c:=p;
+ fold c.inv;
+ assert c.len()==old(len())+1
+ fold inv;
+ }
+
+ method addLast(x:int)
+ requires inv;
+ ensures inv;
+ ensures len()==old(len())+1 && get(old(len()))==x;
+ ensures (forall i:int :: 0<=i && i<old(len()) ==> get(i)==old(get(i)));
+ {
+ unfold inv;
+ if(c==null)
+ {
+ c:=new Node;
+ c.v:=x; c.n:=null;
+ fold c.inv;
+ }
+ else
+ {
+ call c.addLast(x);
+ }
+ fold inv;
+ }
+
+ method append(p:List)
+ requires inv && p!=null && p.inv;
+ ensures inv;
+ ensures len()==old(len()+p.len());
+ ensures (forall i in [0..old(len())] :: get(i)==old(get(i)));
+ ensures (forall i in [old(len())..len()] :: get(i)==old(p.get(i-len())));
+ {
+ unfold inv;
+ if(c==null)
+ {
+ unfold p.inv;
+ c:=p.c;
+ }
+ else
+ {
+ call c.append(p);
+ }
+ fold inv;
+ }
+
+ method remove(i:int)
+ requires inv && i>=0 && i<len();
+ ensures inv;
+ ensures len()==old(len())-1;
+ ensures (forall j in [0..i] :: get(j)==old(get(j)));
+ ensures (forall j in [i..len()] :: get(j)==old(get(j+1)));
+ {
+ unfold inv;
+ if(i==0)
+ {
+ unfold c.inv;
+ c:=c.n;
+ }
+ else
+ {
+ call c.remove(i-1);
+ }
+ fold inv;
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/predicates/LinkedList-various.output.txt b/Chalice/tests/predicates/LinkedList-various.output.txt new file mode 100644 index 00000000..a8a90bb8 --- /dev/null +++ b/Chalice/tests/predicates/LinkedList-various.output.txt @@ -0,0 +1,4 @@ +Verification of LinkedList-various.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/aux-info.output.txt b/Chalice/tests/predicates/aux-info.output.txt index ae84772b..3d873f60 100644 --- a/Chalice/tests/predicates/aux-info.output.txt +++ b/Chalice/tests/predicates/aux-info.output.txt @@ -1,4 +1,4 @@ Verification of aux-info.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/framing-fields.chalice b/Chalice/tests/predicates/framing-fields.chalice index ce168f26..6cfd4607 100644 --- a/Chalice/tests/predicates/framing-fields.chalice +++ b/Chalice/tests/predicates/framing-fields.chalice @@ -11,9 +11,6 @@ class C {
method M (x:List, y:List)
requires x!=null && y!=null && x!=y && x.valid && y.valid;
- requires unfolding x.valid in x.next!=y;
- requires unfolding y.valid in y.next!=x;
- // the two requirements above are needed, otherwise Chalice cannot prove that the two lists are disjoint
{
var i: int := unfolding x.valid in x.value;
var j: int := unfolding y.valid in y.value;
diff --git a/Chalice/tests/predicates/framing-fields.output.txt b/Chalice/tests/predicates/framing-fields.output.txt index 3a7ea2ba..f1b426c6 100644 --- a/Chalice/tests/predicates/framing-fields.output.txt +++ b/Chalice/tests/predicates/framing-fields.output.txt @@ -1,5 +1,5 @@ Verification of framing-fields.chalice using parameters=""
- 22.5: Assertion might not hold. The expression at 22.12 might not evaluate to true. + 19.5: Assertion might not hold. The expression at 19.12 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/framing-functions.output.txt b/Chalice/tests/predicates/framing-functions.output.txt index 01bdd7bb..2a3426c9 100644 --- a/Chalice/tests/predicates/framing-functions.output.txt +++ b/Chalice/tests/predicates/framing-functions.output.txt @@ -2,4 +2,4 @@ Verification of framing-functions.chalice using parameters="" 23.5: Assertion might not hold. The expression at 23.12 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/list-reverse-extra-unfold-fold.chalice b/Chalice/tests/predicates/list-reverse-extra-unfold-fold.chalice new file mode 100644 index 00000000..8467ce4c --- /dev/null +++ b/Chalice/tests/predicates/list-reverse-extra-unfold-fold.chalice @@ -0,0 +1,51 @@ +class Node {
+ var next : Node;
+ var val : int;
+
+ predicate list {
+ acc(next) && acc(val) && (next!=null ==> next.list)
+ }
+
+ function vals() : seq<int>
+ requires list
+ {
+ unfolding list in (next == null ? [val] : [val] ++ next.vals())
+ }
+
+ function reverse_vals() : seq<int>
+ requires list
+ {
+ unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])
+ }
+
+ method reverse_in_place() returns (r:Node)
+ requires list;
+ ensures r != null && r.list;
+ ensures r.vals() == old(this.reverse_vals());
+ {
+ var l : Node := this;
+ r := null;
+
+ while (l != null)
+ invariant l!=null ==> l.list;
+ invariant r!=null ==> r.list;
+ invariant old(this.reverse_vals()) == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
+ {
+ var y: Node;
+ if (r != null) {
+ unfold r.list; fold r.list;
+ }
+ unfold l.list;
+ if (l.next != null) {
+ unfold l.next.list; fold l.next.list;
+ }
+
+
+ y := l.next;
+ l.next := r;
+ r := l;
+ fold r.list;
+ l := y;
+ }
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/predicates/list-reverse-extra-unfold-fold.output.txt b/Chalice/tests/predicates/list-reverse-extra-unfold-fold.output.txt new file mode 100644 index 00000000..6d2967f5 --- /dev/null +++ b/Chalice/tests/predicates/list-reverse-extra-unfold-fold.output.txt @@ -0,0 +1,4 @@ +Verification of list-reverse-extra-unfold-fold.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/mutual-dependence.output.txt b/Chalice/tests/predicates/mutual-dependence.output.txt index a35556a9..263084ac 100644 --- a/Chalice/tests/predicates/mutual-dependence.output.txt +++ b/Chalice/tests/predicates/mutual-dependence.output.txt @@ -2,4 +2,4 @@ Verification of mutual-dependence.chalice using parameters="" 16.5: Assertion might not hold. The expression at 16.12 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/setset.output.txt b/Chalice/tests/predicates/setset.output.txt index c20911f0..b2e963ee 100644 --- a/Chalice/tests/predicates/setset.output.txt +++ b/Chalice/tests/predicates/setset.output.txt @@ -5,4 +5,4 @@ Verification of setset.chalice using parameters="" The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 27.3: The end of method main is unreachable. -Boogie program verifier finished with 1 errors and 1 smoke test warnings.
+Boogie program verifier finished with 1 errors and 1 smoke test warnings
diff --git a/Chalice/tests/predicates/test.chalice b/Chalice/tests/predicates/test.chalice index 6c416671..9477caa6 100644 --- a/Chalice/tests/predicates/test.chalice +++ b/Chalice/tests/predicates/test.chalice @@ -30,9 +30,6 @@ class List fork t:=skip();
// mask: value=0,p=100, secmask: -
assert unfolding P in value==old(value);
- // ERROR: Chalice currently cannot verify this example, as there is neither
- // primary nor secondary permission available to value directly before the
- // assertion
}
}
diff --git a/Chalice/tests/predicates/test.output.txt b/Chalice/tests/predicates/test.output.txt index e05e1b4e..8b97e503 100644 --- a/Chalice/tests/predicates/test.output.txt +++ b/Chalice/tests/predicates/test.output.txt @@ -1,5 +1,4 @@ Verification of test.chalice using parameters=""
- 32.5: Assertion might not hold. The expression at 32.12 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test1.output.txt b/Chalice/tests/predicates/test1.output.txt index 73be63ec..56888ecb 100644 --- a/Chalice/tests/predicates/test1.output.txt +++ b/Chalice/tests/predicates/test1.output.txt @@ -1,4 +1,4 @@ Verification of test1.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test10.output.txt b/Chalice/tests/predicates/test10.output.txt index d38b56a0..c043cbed 100644 --- a/Chalice/tests/predicates/test10.output.txt +++ b/Chalice/tests/predicates/test10.output.txt @@ -1,4 +1,4 @@ Verification of test10.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test2.output.txt b/Chalice/tests/predicates/test2.output.txt index d0bed944..780c15ef 100644 --- a/Chalice/tests/predicates/test2.output.txt +++ b/Chalice/tests/predicates/test2.output.txt @@ -1,4 +1,4 @@ Verification of test2.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test3.output.txt b/Chalice/tests/predicates/test3.output.txt index 7e4e49d6..2753e3f5 100644 --- a/Chalice/tests/predicates/test3.output.txt +++ b/Chalice/tests/predicates/test3.output.txt @@ -1,4 +1,4 @@ Verification of test3.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test4.output.txt b/Chalice/tests/predicates/test4.output.txt index 5268bec7..08a565c8 100644 --- a/Chalice/tests/predicates/test4.output.txt +++ b/Chalice/tests/predicates/test4.output.txt @@ -2,4 +2,4 @@ Verification of test4.chalice using parameters="" 54.2: Assertion might not hold. The expression at 54.9 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test7.output.txt b/Chalice/tests/predicates/test7.output.txt index 46ac796c..e66a1d75 100644 --- a/Chalice/tests/predicates/test7.output.txt +++ b/Chalice/tests/predicates/test7.output.txt @@ -13,4 +13,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 62.3: The end of method uf0 is unreachable. 86.3: The end of method uf3 is unreachable. -Boogie program verifier finished with 7 errors and 3 smoke test warnings.
+Boogie program verifier finished with 7 errors and 3 smoke test warnings
diff --git a/Chalice/tests/predicates/test8.output.txt b/Chalice/tests/predicates/test8.output.txt index 881b2ef0..567d2894 100644 --- a/Chalice/tests/predicates/test8.output.txt +++ b/Chalice/tests/predicates/test8.output.txt @@ -1,4 +1,4 @@ Verification of test8.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/unfolding.chalice b/Chalice/tests/predicates/unfolding.chalice index f01b237d..6b276a04 100644 --- a/Chalice/tests/predicates/unfolding.chalice +++ b/Chalice/tests/predicates/unfolding.chalice @@ -14,6 +14,7 @@ class Cell { method test2()
requires p
+ ensures p
{
var tmp: int := unfolding p in value;
var tmp2: int := unfolding p in value;
diff --git a/Chalice/tests/predicates/unfolding.output.txt b/Chalice/tests/predicates/unfolding.output.txt index 4a1ebbde..7ff49106 100644 --- a/Chalice/tests/predicates/unfolding.output.txt +++ b/Chalice/tests/predicates/unfolding.output.txt @@ -2,4 +2,4 @@ Verification of unfolding.chalice using parameters="" 12.5: Assertion might not hold. The expression at 12.12 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
|