diff options
Diffstat (limited to 'Chalice/tests/general-tests')
19 files changed, 327 insertions, 11 deletions
diff --git a/Chalice/tests/general-tests/FunctionPostcondition.chalice b/Chalice/tests/general-tests/FunctionPostcondition.chalice new file mode 100644 index 00000000..7fd95b05 --- /dev/null +++ b/Chalice/tests/general-tests/FunctionPostcondition.chalice @@ -0,0 +1,10 @@ +// this test is for function postconditions
+
+class FunctionPostconditions
+{
+ predicate valid { true }
+
+ function t1(): int
+ ensures unfolding valid in true;
+ { 1 }
+}
diff --git a/Chalice/tests/general-tests/FunctionPostcondition.output.txt b/Chalice/tests/general-tests/FunctionPostcondition.output.txt new file mode 100644 index 00000000..3244dc57 --- /dev/null +++ b/Chalice/tests/general-tests/FunctionPostcondition.output.txt @@ -0,0 +1,4 @@ +Verification of FunctionPostcondition.chalice using parameters=""
+
+The program did not typecheck.
+8.5: the postcondition of functions cannot contain unfolding expressions at the moment
diff --git a/Chalice/tests/general-tests/ImplicitLocals.output.txt b/Chalice/tests/general-tests/ImplicitLocals.output.txt index db26bba6..8e59a2b0 100644 --- a/Chalice/tests/general-tests/ImplicitLocals.output.txt +++ b/Chalice/tests/general-tests/ImplicitLocals.output.txt @@ -1,4 +1,4 @@ Verification of ImplicitLocals.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/general-tests/LoopLockChange.output.txt b/Chalice/tests/general-tests/LoopLockChange.output.txt index 19e84f93..ccd9a36a 100644 --- a/Chalice/tests/general-tests/LoopLockChange.output.txt +++ b/Chalice/tests/general-tests/LoopLockChange.output.txt @@ -9,4 +9,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 10.5: The statements after the while-loop are unreachable. 75.5: Assumption introduces a contradiction. -Boogie program verifier finished with 3 errors and 3 smoke test warnings.
+Boogie program verifier finished with 3 errors and 3 smoke test warnings
diff --git a/Chalice/tests/general-tests/RockBand-automagic.output.txt b/Chalice/tests/general-tests/RockBand-automagic.output.txt index 2e62b457..652213d9 100644 --- a/Chalice/tests/general-tests/RockBand-automagic.output.txt +++ b/Chalice/tests/general-tests/RockBand-automagic.output.txt @@ -1,4 +1,4 @@ Verification of RockBand-automagic.chalice using parameters="-checkLeaks -defaults -autoFold -autoMagic"
-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/general-tests/SmokeTestTest.output.txt b/Chalice/tests/general-tests/SmokeTestTest.output.txt index 3d1cd786..1ad5f926 100644 --- a/Chalice/tests/general-tests/SmokeTestTest.output.txt +++ b/Chalice/tests/general-tests/SmokeTestTest.output.txt @@ -20,4 +20,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 116.3: Predicate Cell.valid is equivalent to false. 121.1: Where clause of channel C is equivalent to false. -Boogie program verifier finished with 1 errors and 16 smoke test warnings.
+Boogie program verifier finished with 1 errors and 16 smoke test warnings
diff --git a/Chalice/tests/general-tests/cell-defaults.output.txt b/Chalice/tests/general-tests/cell-defaults.output.txt index 138a5717..fd748230 100644 --- a/Chalice/tests/general-tests/cell-defaults.output.txt +++ b/Chalice/tests/general-tests/cell-defaults.output.txt @@ -7,4 +7,4 @@ Verification of cell-defaults.chalice using parameters="-defaults -autoFold -aut The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 125.3: The end of method main2 is unreachable. -Boogie program verifier finished with 3 errors and 1 smoke test warnings.
+Boogie program verifier finished with 3 errors and 1 smoke test warnings
diff --git a/Chalice/tests/general-tests/counter.output.txt b/Chalice/tests/general-tests/counter.output.txt index 3c7f78b0..53bcd98d 100644 --- a/Chalice/tests/general-tests/counter.output.txt +++ b/Chalice/tests/general-tests/counter.output.txt @@ -14,4 +14,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 137.7: The begging of the lock-block is unreachable. 142.3: The end of method nestedBad3 is unreachable. -Boogie program verifier finished with 6 errors and 5 smoke test warnings.
+Boogie program verifier finished with 6 errors and 5 smoke test warnings
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
diff --git a/Chalice/tests/general-tests/nestedPredicates.chalice b/Chalice/tests/general-tests/nestedPredicates.chalice new file mode 100644 index 00000000..8afbff5c --- /dev/null +++ b/Chalice/tests/general-tests/nestedPredicates.chalice @@ -0,0 +1,114 @@ +/* Recursive implementation and specification of a linked list. */
+
+class Node {
+ var next: Node;
+ var value: int;
+
+ predicate valid {
+ rd*(next) && rd*(value) && (next!=null ==> next.valid)
+ }
+
+ method testNestingUnfold()
+ requires acc(this.valid)
+ {
+ unfold this.valid;
+ assert this != this.next;
+ if(this.next != null) {
+ unfold this.next.valid;
+ assert this.next != this.next.next;
+ assert this != this.next.next;
+ }
+ }
+
+ method testNestingFold() // this test shows that we build in the assumption that predicate instances with infinite expansions cannot be exist (in reachable code)
+ requires rd*(this.next) && rd*(this.value) && rd*(this.next.next) && rd*(this.next.value) && this.next != null && this.next.next != null && this.next.next.valid
+
+ {
+ fold this.next.valid;
+ assert this.next != this.next.next; // definition of valid "proves" that this.next and this.next.next cannot be aliases
+ fold this.valid;
+ assert this != this.next;
+ assert this != this.next.next;
+ }
+
+ method testNestingUnfolding()
+ requires acc(this.valid)
+ {
+ assert this != (unfolding this.valid in this.next);
+ if((unfolding this.valid in this.next) != null) {
+ assert (unfolding this.valid in this.next) != (unfolding this.valid in (unfolding this.next.valid in this.next.next));
+ assert this != (unfolding this.valid in (unfolding this.next.valid in this.next.next));
+ }
+ }
+
+ predicate p {
+ rd*(next) && rd*(value) && (next!=null ==> next.q)
+ }
+
+ predicate q {
+ rd*(next) && rd*(value) && (next!=null ==> next.p)
+ }
+
+ method testNestingUnfoldTwo()
+ requires acc(this.p)
+ {
+ unfold this.p;
+ assert this != this.next; // should fail
+ if(this.next != null) {
+ unfold this.next.q;
+ assert this.next != this.next.next; // should fail
+ assert this != this.next.next; // should succeed
+ }
+ }
+
+ method testNestingFoldTwo() // this test shows that we build in the assumption that predicate instances with infinite expansions cannot be exist (in reachable code)
+ requires rd*(this.next) && rd*(this.value) && rd*(this.next.next) && rd*(this.next.value) && this.next != null && this.next.next != null && this.next.next.p
+
+ {
+ fold this.next.q;
+ assert this != this.next; // should fail
+ assert this.next != this.next.next; // should fail
+ assert this != this.next.next; // should fail
+ }
+
+ method testNestingFoldThree() // this test shows that we build in the assumption that predicate instances with infinite expansions cannot be exist (in reachable code)
+ requires rd*(this.next) && rd*(this.value) && rd*(this.next.next) && rd*(this.next.value) && this.next != null && this.next.next != null && this.next.next.p
+
+ {
+ fold this.next.q;
+ fold this.p;
+ assert this != this.next; // should succeed, since this == this.next ==> this == this.next.next
+ assert this.next != this.next.next; // should fail - we haven't seen a cycle which would follow from this fact
+ assert this != this.next.next; // should succeed
+ }
+
+ method testNestingUnfoldingTwo()
+ requires acc(this.p)
+ {
+ assert this != (unfolding this.p in this.next); // should fail
+ if((unfolding this.p in this.next) != null) {
+ assert (unfolding this.p in this.next) != (unfolding this.p in (unfolding this.next.q in this.next.next)); // should fail
+ assert this != (unfolding this.p in (unfolding this.next.q in this.next.next)); // should succeed
+ }
+ }
+
+ method testNestingUnfoldingPrecondition(x: Node)
+ requires acc(this.valid) && (unfolding this.valid in this.next == x);
+ {
+ assert this != x;
+ }
+
+ function getNext() : Node
+ requires this.valid;
+ {
+ unfolding this.valid in this.next
+ }
+
+ method testNestingUnfoldingPostcondition(x: Node)
+ requires acc(this.valid);
+ ensures acc(this.valid) && (unfolding this.valid in true) && this != this.getNext()
+ {
+ // nothing
+ }
+
+}
\ No newline at end of file diff --git a/Chalice/tests/general-tests/nestedPredicates.output.txt b/Chalice/tests/general-tests/nestedPredicates.output.txt new file mode 100644 index 00000000..635ae780 --- /dev/null +++ b/Chalice/tests/general-tests/nestedPredicates.output.txt @@ -0,0 +1,12 @@ +Verification of nestedPredicates.chalice using parameters=""
+
+ 56.7: Assertion might not hold. The expression at 56.14 might not evaluate to true. + 59.9: Assertion might not hold. The expression at 59.16 might not evaluate to true. + 69.7: Assertion might not hold. The expression at 69.14 might not evaluate to true. + 70.7: Assertion might not hold. The expression at 70.14 might not evaluate to true. + 71.7: Assertion might not hold. The expression at 71.14 might not evaluate to true. + 81.7: Assertion might not hold. The expression at 81.14 might not evaluate to true. + 88.7: Assertion might not hold. The expression at 88.14 might not evaluate to true. + 90.9: Assertion might not hold. The expression at 90.16 might not evaluate to true. + +Boogie program verifier finished with 8 errors and 0 smoke test warnings
diff --git a/Chalice/tests/general-tests/prog1.output.txt b/Chalice/tests/general-tests/prog1.output.txt index 630ecdfa..c6c5fe0e 100644 --- a/Chalice/tests/general-tests/prog1.output.txt +++ b/Chalice/tests/general-tests/prog1.output.txt @@ -16,4 +16,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 73.3: The end of method main5 is unreachable. 78.3: The end of method main6 is unreachable. -Boogie program verifier finished with 7 errors and 6 smoke test warnings.
+Boogie program verifier finished with 7 errors and 6 smoke test warnings
diff --git a/Chalice/tests/general-tests/prog2.output.txt b/Chalice/tests/general-tests/prog2.output.txt index 68cd4870..da8dcf22 100644 --- a/Chalice/tests/general-tests/prog2.output.txt +++ b/Chalice/tests/general-tests/prog2.output.txt @@ -9,4 +9,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 20.3: The end of method Caller1 is unreachable. 69.3: The end of method M2 is unreachable. -Boogie program verifier finished with 4 errors and 2 smoke test warnings.
+Boogie program verifier finished with 4 errors and 2 smoke test warnings
diff --git a/Chalice/tests/general-tests/prog3.output.txt b/Chalice/tests/general-tests/prog3.output.txt index 18d05658..286b9248 100644 --- a/Chalice/tests/general-tests/prog3.output.txt +++ b/Chalice/tests/general-tests/prog3.output.txt @@ -8,4 +8,4 @@ Verification of prog3.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. 191.5: The statements after the method call statement are unreachable. -Boogie program verifier finished with 4 errors and 1 smoke test warnings.
+Boogie program verifier finished with 4 errors and 1 smoke test warnings
diff --git a/Chalice/tests/general-tests/prog4.output.txt b/Chalice/tests/general-tests/prog4.output.txt index 9415df7c..4ab057dd 100644 --- a/Chalice/tests/general-tests/prog4.output.txt +++ b/Chalice/tests/general-tests/prog4.output.txt @@ -11,4 +11,4 @@ Verification of prog4.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. 2.3: The end of method M is unreachable. -Boogie program verifier finished with 7 errors and 1 smoke test warnings.
+Boogie program verifier finished with 7 errors and 1 smoke test warnings
diff --git a/Chalice/tests/general-tests/quantifiers.output.txt b/Chalice/tests/general-tests/quantifiers.output.txt index 2f325c42..f05847b6 100644 --- a/Chalice/tests/general-tests/quantifiers.output.txt +++ b/Chalice/tests/general-tests/quantifiers.output.txt @@ -2,4 +2,4 @@ Verification of quantifiers.chalice using parameters="" 57.29: The heap of the callee might not be strictly smaller than the heap of the caller. -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/general-tests/triggers.chalice b/Chalice/tests/general-tests/triggers.chalice new file mode 100644 index 00000000..08a6a7dd --- /dev/null +++ b/Chalice/tests/general-tests/triggers.chalice @@ -0,0 +1,81 @@ +// this test is for the automatic trigger generation
+
+class Triggers
+{
+ var next : Triggers // to allow recursive definitions
+
+ predicate valid { acc(next) && next != null && next.valid } // intentionally doesn't terminate - allows function definitions to be unknown
+
+ function f(x,y,z : int):bool
+ requires valid
+ {
+ unfolding valid in next.f(x,y,z) // unknown definition
+ }
+
+ function h(x,y,z : int):bool
+ requires valid
+ {
+ unfolding valid in next.h(x,y,z) // unknown definition
+ }
+
+ function g(x : int) : bool
+ requires valid
+ {
+ unfolding valid in next.g(x) // unknown definition
+ }
+
+ function i(x:int, y:bool) : bool
+ requires valid
+ {
+ unfolding valid in next.i(x,y) // unknown definition
+ }
+
+
+ method triggers_one()
+ requires valid
+ requires (forall a : int :: !(g(a) ==> false))
+ ensures valid
+ ensures (forall b : int :: g(b))
+ { }
+
+ method triggers_two()
+ requires valid
+ requires (forall a,b,c : int :: ( g(a) && f(a,b,c)))
+ ensures valid
+ ensures (forall x,y,z : int :: f(x,y,z))
+ ensures (forall w : int :: (g(w))) // fails because there isn't a good enough trigger for finding g(w)
+ { }
+
+ method triggers_three()
+ requires valid
+ requires (forall a : int :: ( g(a) && (forall b,c : int :: f(a,b,c))))
+ ensures valid
+ ensures (forall x,y,z : int :: f(x,y,z)) // fails because of the trigger chosen for a (g(a)).
+ ensures (forall w : int :: (g(w)))
+ { }
+
+ method triggers_four()
+ requires valid
+ requires (forall a,b,c,d,e:int :: f(a,b,c) && h(b,c,d) && f(c,d,e))
+ ensures valid
+ ensures (forall x,y,z : int :: f(x,y,z)) // fails - not enough triggers
+ ensures (forall x,y,z : int :: f(x,y,z) && f(z,y,x)) // succeeds - {f(a,b,c),f(c,d,e)} is one of the trigger sets which should be found
+ { }
+
+ method triggers_five(c : bool, d : bool)
+ requires c ==> d
+ requires valid
+ requires (forall x : int :: i(x, (c ==> d))) // check that logical operators are suitably avoided in triggers
+ ensures valid
+ ensures i(4,true)
+ { }
+
+ method triggers_six(c : int, d : int)
+ requires c > d
+ requires valid
+ requires (forall x : int :: i(x, (c > d))) // check that logical operators are suitably avoided in triggers
+ ensures valid
+ ensures i(4,true)
+ { }
+
+}
\ No newline at end of file diff --git a/Chalice/tests/general-tests/triggers.output.txt b/Chalice/tests/general-tests/triggers.output.txt new file mode 100644 index 00000000..3fae3c21 --- /dev/null +++ b/Chalice/tests/general-tests/triggers.output.txt @@ -0,0 +1,7 @@ +Verification of triggers.chalice using parameters=""
+
+ 41.3: The postcondition at 46.14 might not hold. The expression at 46.14 might not evaluate to true. + 49.3: The postcondition at 53.14 might not hold. The expression at 53.14 might not evaluate to true. + 57.3: The postcondition at 61.14 might not hold. The expression at 61.14 might not evaluate to true. + +Boogie program verifier finished with 3 errors and 0 smoke test warnings
|