diff options
| author |  Rustan Leino <unknown> | 2013-03-05 16:58:16 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-03-05 16:58:16 -0800 |
| commit | c819fabbb8da669952cb7e2e5937c73ff6dcfabe (patch) | |
| tree | fdfa5ecd7ef81709608d5dcb5ba232611c1b073f /Chalice/tests/predicates | |
| parent | f82dab21f1240fb3f8d67a880f4f93017d85c345 (diff) | |
Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codeplex repositories.
Diffstat (limited to 'Chalice/tests/predicates')
39 files changed, 0 insertions, 957 deletions
diff --git a/Chalice/tests/predicates/FoldUnfoldExperiments.chalice b/Chalice/tests/predicates/FoldUnfoldExperiments.chalice deleted file mode 100644 index 4bead442..00000000 --- a/Chalice/tests/predicates/FoldUnfoldExperiments.chalice +++ /dev/null @@ -1,32 +0,0 @@ -class FoldUnfoldExperiments
-{
- var x:int;
- var y:int;
- predicate X { acc(x) }
- predicate Y { acc(y) }
-
- function getX():int
- requires X;
- { unfolding X in x }
-
- function getY():int
- requires Y;
- { unfolding Y in y }
-
- method setX(v:int)
- requires X;
- ensures X && getX()==v;
- {
- unfold X; x:=v; fold X;
- }
-
- method check()
- requires acc(x) && acc(y);
- ensures acc(y) && y==2 && X && getX()==3;
- {
- x:=1; y:=2;
- fold X; fold Y;
- call setX(3);
- unfold Y;
- }
-}
\ No newline at end of file diff --git a/Chalice/tests/predicates/FoldUnfoldExperiments.output.txt b/Chalice/tests/predicates/FoldUnfoldExperiments.output.txt deleted file mode 100644 index ba48d6f4..00000000 --- a/Chalice/tests/predicates/FoldUnfoldExperiments.output.txt +++ /dev/null @@ -1,4 +0,0 @@ -Verification of FoldUnfoldExperiments.chalice using parameters=""
-
- -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 deleted file mode 100644 index a888b647..00000000 --- a/Chalice/tests/predicates/LinkedList-various.chalice +++ /dev/null @@ -1,176 +0,0 @@ -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 deleted file mode 100644 index a8a90bb8..00000000 --- a/Chalice/tests/predicates/LinkedList-various.output.txt +++ /dev/null @@ -1,4 +0,0 @@ -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.chalice b/Chalice/tests/predicates/aux-info.chalice deleted file mode 100644 index f457c481..00000000 --- a/Chalice/tests/predicates/aux-info.chalice +++ /dev/null @@ -1,33 +0,0 @@ -class Cell {
- var value: int;
-
- predicate p { acc(value,1) }
-
- method test()
- requires p && acc(value,2)
- {
- // previously, the following sequence let to negative secondary permission
- // to the field value.
- fold p
- fold p
- call void()
- call void()
- call void2()
-
- unfold p
- var tmp: int := value
- fold p
- // make sure that at this point we can retain information about the field value
- assert tmp == unfolding p in value
- }
-
- method void()
- requires p
- {}
-
- method void2()
- requires p
- ensures p
- {}
-
-}
diff --git a/Chalice/tests/predicates/aux-info.output.txt b/Chalice/tests/predicates/aux-info.output.txt deleted file mode 100644 index 3d873f60..00000000 --- a/Chalice/tests/predicates/aux-info.output.txt +++ /dev/null @@ -1,4 +0,0 @@ -Verification of aux-info.chalice using parameters=""
-
- -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 deleted file mode 100644 index 6cfd4607..00000000 --- a/Chalice/tests/predicates/framing-fields.chalice +++ /dev/null @@ -1,21 +0,0 @@ -class List
-{
- var value:int;
- var next:List;
- predicate valid { acc(value) && acc(next) && (next!=null ==> next.valid) }
-
- method set(x:int, y:int) requires valid; ensures valid; {}
-}
-
-class C
-{
- method M (x:List, y:List)
- requires x!=null && y!=null && x!=y && x.valid && y.valid;
- {
- var i: int := unfolding x.valid in x.value;
- var j: int := unfolding y.valid in y.value;
- call y.set(0,10);
- assert unfolding x.valid in (i == x.value); // succeeds
- assert unfolding y.valid in (j == y.value); // correctly fails to verify
- }
-}
\ No newline at end of file diff --git a/Chalice/tests/predicates/framing-fields.output.txt b/Chalice/tests/predicates/framing-fields.output.txt deleted file mode 100644 index f1b426c6..00000000 --- a/Chalice/tests/predicates/framing-fields.output.txt +++ /dev/null @@ -1,5 +0,0 @@ -Verification of framing-fields.chalice using parameters=""
-
- 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
diff --git a/Chalice/tests/predicates/framing-functions.chalice b/Chalice/tests/predicates/framing-functions.chalice deleted file mode 100644 index 8b66a473..00000000 --- a/Chalice/tests/predicates/framing-functions.chalice +++ /dev/null @@ -1,25 +0,0 @@ -class List
-{
- var value:int;
- var next:List;
- predicate valid { acc(value) && acc(next) && (next!=null ==> next.valid) }
-
- method set(x:int, y:int) requires valid; ensures valid; {}
-
- function itemAt(i: int): int
- requires valid && 0 <= i;
- { unfolding valid in i == 0 || next == null ? value : next.itemAt(i-1) }
-}
-
-class C
-{
- method M (x:List, y:List)
- requires x!=null && y!=null && x!=y && x.valid && y.valid;
- {
- var i: int := x.itemAt(0);
- var j: int := y.itemAt(0);
- call y.set(0,10);
- assert i==x.itemAt(0); // succeeds
- assert j==y.itemAt(0); // correctly fails to verify
- }
-}
\ No newline at end of file diff --git a/Chalice/tests/predicates/framing-functions.output.txt b/Chalice/tests/predicates/framing-functions.output.txt deleted file mode 100644 index 2a3426c9..00000000 --- a/Chalice/tests/predicates/framing-functions.output.txt +++ /dev/null @@ -1,5 +0,0 @@ -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
diff --git a/Chalice/tests/predicates/generate_reference.bat b/Chalice/tests/predicates/generate_reference.bat deleted file mode 100644 index 6864843c..00000000 --- a/Chalice/tests/predicates/generate_reference.bat +++ /dev/null @@ -1,2 +0,0 @@ -@echo off
-call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/predicates/generate_reference_all.bat b/Chalice/tests/predicates/generate_reference_all.bat deleted file mode 100644 index 6864843c..00000000 --- a/Chalice/tests/predicates/generate_reference_all.bat +++ /dev/null @@ -1,2 +0,0 @@ -@echo off
-call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/predicates/list-reverse-extra-unfold-fold.chalice b/Chalice/tests/predicates/list-reverse-extra-unfold-fold.chalice deleted file mode 100644 index 8467ce4c..00000000 --- a/Chalice/tests/predicates/list-reverse-extra-unfold-fold.chalice +++ /dev/null @@ -1,51 +0,0 @@ -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 deleted file mode 100644 index 6d2967f5..00000000 --- a/Chalice/tests/predicates/list-reverse-extra-unfold-fold.output.txt +++ /dev/null @@ -1,4 +0,0 @@ -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.chalice b/Chalice/tests/predicates/mutual-dependence.chalice deleted file mode 100644 index a0939607..00000000 --- a/Chalice/tests/predicates/mutual-dependence.chalice +++ /dev/null @@ -1,24 +0,0 @@ -class Cell {
- var value: int;
- var next: Cell;
-
- predicate p { q }
- predicate q { acc(value) && acc(next) && (next != null ==> next.p) }
-
- method test()
- requires acc(this.*)
- {
- value := 1
- next := null
- fold q
- fold p
- call void()
- assert unfolding p in unfolding q in value == 1 // ERROR: should not verify
- }
-
- method void()
- requires p
- ensures p
- {}
-
-}
diff --git a/Chalice/tests/predicates/mutual-dependence.output.txt b/Chalice/tests/predicates/mutual-dependence.output.txt deleted file mode 100644 index 263084ac..00000000 --- a/Chalice/tests/predicates/mutual-dependence.output.txt +++ /dev/null @@ -1,5 +0,0 @@ -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
diff --git a/Chalice/tests/predicates/reg_test.bat b/Chalice/tests/predicates/reg_test.bat deleted file mode 100644 index 6864843c..00000000 --- a/Chalice/tests/predicates/reg_test.bat +++ /dev/null @@ -1,2 +0,0 @@ -@echo off
-call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/predicates/reg_test_all.bat b/Chalice/tests/predicates/reg_test_all.bat deleted file mode 100644 index 6864843c..00000000 --- a/Chalice/tests/predicates/reg_test_all.bat +++ /dev/null @@ -1,2 +0,0 @@ -@echo off
-call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/predicates/setset.chalice b/Chalice/tests/predicates/setset.chalice deleted file mode 100644 index 512c65c1..00000000 --- a/Chalice/tests/predicates/setset.chalice +++ /dev/null @@ -1,57 +0,0 @@ -class Node {
- var value: int;
-
- method init(v: int)
- requires acc(value)
- ensures valid
- {
- value := v
- fold this.valid
- }
-
- function get():int requires valid { unfolding valid in value }
-
- method set(v: int)
- requires valid
- ensures valid && get() == v
- {
- unfold valid
- value := v
- fold valid
- }
-
- predicate valid {
- acc(value)
- }
-
- method main(x: Node, y: Node)
- requires x != null && y != null
- requires x.valid && y.valid
- {
- call x.set(3)
- call y.set(3)
- call x.set(3)
- call y.set(3)
- call x.set(3)
- call y.set(3)
- call x.set(3)
- unfold x.valid
- x.value := 3
- fold x.valid
- call y.set(3)
- call x.set(3)
- call y.set(3)
- unfold x.valid
- x.value := 3
- fold x.valid
- unfold x.valid
- x.value := 3
- fold x.valid
- call x.set(3)
- call y.set(3)
- call x.set(4)
-
- assert y.get() == 3
- assert x.get() == 3 // error: should fail
- }
-}
\ No newline at end of file diff --git a/Chalice/tests/predicates/setset.output.txt b/Chalice/tests/predicates/setset.output.txt deleted file mode 100644 index b2e963ee..00000000 --- a/Chalice/tests/predicates/setset.output.txt +++ /dev/null @@ -1,8 +0,0 @@ -Verification of setset.chalice using parameters=""
-
- 55.5: Assertion might not hold. The expression at 55.12 might not evaluate to true. - -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
diff --git a/Chalice/tests/predicates/test.bat b/Chalice/tests/predicates/test.bat deleted file mode 100644 index 6864843c..00000000 --- a/Chalice/tests/predicates/test.bat +++ /dev/null @@ -1,2 +0,0 @@ -@echo off
-call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/predicates/test.chalice b/Chalice/tests/predicates/test.chalice deleted file mode 100644 index 9477caa6..00000000 --- a/Chalice/tests/predicates/test.chalice +++ /dev/null @@ -1,35 +0,0 @@ -class List
-{
- var value:int;
- var next:List;
-
- predicate inv { acc(value) && acc(next) && (next!=null ==> next.inv) }
-
- function len():int
- requires inv;
- {
- unfolding inv in (next==null) ? 1 : (1+next.len())
- }
-
- predicate P { acc(value,50) }
-
- method skip()
- requires P; ensures P
- {}
-
- method goo()
- requires acc(value);
- {
- // mask: value=100, secmask: -
- fold P;
- // mask: value=50,p=100, secmask: value=50
- call skip();
- // mask: value=50,p=100, secmask: -
- fold P;
- // mask: value=0,p=200, secmask: value=50
- fork t:=skip();
- // mask: value=0,p=100, secmask: -
- assert unfolding P in value==old(value);
- }
-
-}
diff --git a/Chalice/tests/predicates/test.output.txt b/Chalice/tests/predicates/test.output.txt deleted file mode 100644 index 8b97e503..00000000 --- a/Chalice/tests/predicates/test.output.txt +++ /dev/null @@ -1,4 +0,0 @@ -Verification of test.chalice using parameters=""
-
- -Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test1.chalice b/Chalice/tests/predicates/test1.chalice deleted file mode 100644 index 7dbde565..00000000 --- a/Chalice/tests/predicates/test1.chalice +++ /dev/null @@ -1,50 +0,0 @@ -class List
-{
- var value:int;
- var next:List;
-
- predicate inv { acc(value) && acc(next) && (next!=null ==> next.inv) }
-
- function get():int
- requires inv;
- { unfolding inv in value }
-
- // the purpose of this method is to test whether the methodology can roll back correctly the secondary mask:
- // s0 unf s1 unf s2 fold, should roll back to state s1 and not s0
- // note also the unfolding expression in the precondition: the fact that next!=null must be known in the body of the method
- // this means that the secondary mask must start off containing this.next, according to the proposal
- method foo()
- requires inv && unfolding inv in next!=null;
- ensures inv && unfolding inv in next!=null;
- {
- unfold inv;
- value:=0;
- unfold next.inv;
- next.value:=1;
- fold next.inv;
- assert next.get()==1;
- assert value==0;
- fold inv;
- assert get()==0;
- assert unfolding inv in next!=null && next.get()==1;
- assert unfolding inv in next.get()==1;
- }
-
- // this method tests whether the methodology works correctly when (un)folds happen on statically unknown objects
- method goo(a:List, b:List, c:bool)
- requires a!=null && b!=null && a.inv && b.inv;
- {
- var z:List;
- unfold a.inv;
- unfold b.inv;
- a.value:=0;
- b.value:=1;
- if(c) { z:=a } else { z:=b }
- fold z.inv;
- assert c ==> a.inv && a.get()==0;
- assert !c ==> b.inv && b.get()==1;
- unfold z.inv;
- assert a.value==0;
- assert b.value==1;
- }
-}
\ No newline at end of file diff --git a/Chalice/tests/predicates/test1.output.txt b/Chalice/tests/predicates/test1.output.txt deleted file mode 100644 index 56888ecb..00000000 --- a/Chalice/tests/predicates/test1.output.txt +++ /dev/null @@ -1,4 +0,0 @@ -Verification of test1.chalice using parameters=""
-
- -Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test10.chalice b/Chalice/tests/predicates/test10.chalice deleted file mode 100644 index 7d45914c..00000000 --- a/Chalice/tests/predicates/test10.chalice +++ /dev/null @@ -1,18 +0,0 @@ -class List
-{
- var value:int;
- var next:List;
-
- predicate inv { acc(value) && acc(next) && (next!=null ==> next.inv) }
-
- function get():int
- requires inv;
- { unfolding inv in value }
-
- method foo()
- requires inv && unfolding inv in next!=null;
- ensures inv && unfolding inv in next!=null;
- {
- assert unfolding inv in unfolding next.inv in true;
- }
-}
\ No newline at end of file diff --git a/Chalice/tests/predicates/test10.output.txt b/Chalice/tests/predicates/test10.output.txt deleted file mode 100644 index c043cbed..00000000 --- a/Chalice/tests/predicates/test10.output.txt +++ /dev/null @@ -1,4 +0,0 @@ -Verification of test10.chalice using parameters=""
-
- -Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test2.chalice b/Chalice/tests/predicates/test2.chalice deleted file mode 100644 index f93a1eeb..00000000 --- a/Chalice/tests/predicates/test2.chalice +++ /dev/null @@ -1,55 +0,0 @@ -class FoldUnfoldExperiments
-{
- var x:int;
- var y:int;
- var z:int;
- var w:int;
- predicate X { acc(x) }
- predicate Y { acc(y) }
- predicate Z { acc(z) }
-
- function getX():int
- requires X;
- { unfolding X in x }
-
- function getY():int
- requires Y;
- { unfolding Y in y }
-
- function getZ():int
- requires Z;
- { unfolding Z in z }
-
- method setX(v:int)
- requires X;
- ensures X && getX()==v;
- {
- unfold X; x:=v; fold X;
- }
-
- // this method checks if the methodology frames correctly around a method call: what happens with folded data and unfolded data
- // also: what happens if we have folded data during the call, that we unfold after the call
- method check()
- requires acc(x) && acc(y) && acc(z) && acc(w);
- ensures acc(y) && y==2 && X && getX()==3 && Z && getZ()==4 && acc(w) && w==10;
- {
- x:=1; y:=2; z:=4; w:=10;
- fold X; fold Y; fold Z;
- call setX(3);
- unfold Y;
- }
-
- // this method checks that method calls do not interfere with the correct handling of folds and unfolds
- method check1()
- requires X && acc(y) && y==1;
- ensures acc(y) && y==1 && X && getX()==200;
- {
- call setX(10);
- fold Y;
- call setX(100);
- unfold Y;
- fold Y;
- unfold Y;
- call setX(200);
- }
-}
\ No newline at end of file diff --git a/Chalice/tests/predicates/test2.output.txt b/Chalice/tests/predicates/test2.output.txt deleted file mode 100644 index 780c15ef..00000000 --- a/Chalice/tests/predicates/test2.output.txt +++ /dev/null @@ -1,4 +0,0 @@ -Verification of test2.chalice using parameters=""
-
- -Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test3.chalice b/Chalice/tests/predicates/test3.chalice deleted file mode 100644 index 2a364fee..00000000 --- a/Chalice/tests/predicates/test3.chalice +++ /dev/null @@ -1,29 +0,0 @@ -class Unsound
-{
- var value:int;
-
- predicate inv { acc(value) }
-
- function get():int
- requires inv;
- {
- unfolding inv in value
- }
-
- method set(newval:int)
- requires inv;
- ensures inv && get()==newval;
- {
- unfold inv;
- value:=newval;
- fold inv;
- }
-
- method test()
- requires inv;
- {
- call set(3);
- call set(4);
- // at this point, Chalice used to be able to prove false
- }
-}
\ No newline at end of file diff --git a/Chalice/tests/predicates/test3.output.txt b/Chalice/tests/predicates/test3.output.txt deleted file mode 100644 index 2753e3f5..00000000 --- a/Chalice/tests/predicates/test3.output.txt +++ /dev/null @@ -1,4 +0,0 @@ -Verification of test3.chalice using parameters=""
-
- -Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test4.chalice b/Chalice/tests/predicates/test4.chalice deleted file mode 100644 index 201b643d..00000000 --- a/Chalice/tests/predicates/test4.chalice +++ /dev/null @@ -1,56 +0,0 @@ -class Cell
-{
- var value:int;
-
- predicate P { acc(value,50) }
-
- function get():int
- requires P;
- {
- unfolding P in value
- }
-
- method boom(x:Cell, y:Cell)
- requires x!=null && y!=null && x.P && y.P;
- ensures x.P && y.P && (x==y ==> x.get()==100) && (x!=y ==> x.get()==old(x.get()));
- {
- if(x==y)
- {
- unfold x.P; unfold x.P;
- y.value:=100;
- fold y.P; fold y.P;
- }
- }
-
- method skip()
- requires P;
- ensures P;
- {}
-
- // is the bookkeeping correct when calculating the secondary mask?
- // fold happens once on a statically unknown object
- // intermediate calls to skip happen in all examples to create artificial "changes" to the heap,
- // thereby testing framing in the bookkeeping of folds/unfolds
- method foo(z:Cell)
- requires acc(value,50) && value==2 && z!=null && acc(z.value,50);
- {
- fold z.P;
- call z.skip();
- fold P;
- call boom(this, z);
- assert this!=z ==> unfolding P in value==2;
- assert this==z ==> unfolding P in value==100;
- }
-
- // must fail: give away all permission, even in pieces, and you lose all information about value
- method hoo()
- requires acc(value);
- {
- fold P;
- call skip();
- fold P;
- fork t:=skip();
- call skip ();
- assert unfolding P in value==old(value); // ERROR: should fail
- }
-}
\ No newline at end of file diff --git a/Chalice/tests/predicates/test4.output.txt b/Chalice/tests/predicates/test4.output.txt deleted file mode 100644 index 08a565c8..00000000 --- a/Chalice/tests/predicates/test4.output.txt +++ /dev/null @@ -1,5 +0,0 @@ -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
diff --git a/Chalice/tests/predicates/test7.chalice b/Chalice/tests/predicates/test7.chalice deleted file mode 100644 index 6ad8e592..00000000 --- a/Chalice/tests/predicates/test7.chalice +++ /dev/null @@ -1,109 +0,0 @@ -class C
-{
- var value:int;
-
- predicate inv { acc(value) }
-
- function get():int
- requires inv;
- {
- unfolding inv in value
- }
-
- method set(newval:int)
- requires inv;
- ensures inv && get()==newval;
- {
- unfold inv;
- value:=newval;
- fold inv;
- }
-
- method callmethod0()
- requires inv;
- ensures inv && get()==3;
- {
- call set(3);
- }
-
- method callmethod1()
- {
- call set(3); // ERROR: should fail
- }
-
- method ifc()
- requires inv;
- ensures inv && get()>old(get())
- {
- if(get()>0) { call set(get()+get()); }
- else { call set(2); }
- }
-
- method loop0() returns (r:int)
- requires inv && get()>0;
- ensures inv && r==get();
- {
- r:=0;
- while (r<unfolding inv in value)
- invariant inv && r<=get();
- { r:=r+1; }
- }
-
- method loop1() returns (r:int)
- requires inv && get()>0;
- ensures inv && r==get();
- {
- r:=0;
- while (r<get())
- invariant inv && r<=unfolding inv in value;
- { r:=r+1; }
- }
-
- method uf0()
- requires acc(value);
- {
- assert acc(value);
- fold inv;
- assert acc(value); // ERROR: should fail
- }
-
- method uf1()
- requires acc(value);
- {
- assert acc(value);
- fold inv;
- assert acc(inv);
- }
-
- method uf2()
- requires inv;
- {
- assert inv;
- unfold inv;
- assert acc(value);
- }
-
- method uf3()
- requires inv;
- {
- assert inv;
- unfold inv;
- assert acc(inv); // ERROR: should fail
- }
-
- method badframing0()
- requires get()==2; // ERROR: should fail
- {}
-
- method badframing1()
- requires value==2; // ERROR: should fail
- {}
-
- method badframing2()
- requires acc(value) && get()==2; // ERROR: should fail
- {}
-
- method badframing3()
- requires inv && value==2; // ERROR: should fail
- {}
-}
\ No newline at end of file diff --git a/Chalice/tests/predicates/test7.output.txt b/Chalice/tests/predicates/test7.output.txt deleted file mode 100644 index e66a1d75..00000000 --- a/Chalice/tests/predicates/test7.output.txt +++ /dev/null @@ -1,16 +0,0 @@ -Verification of test7.chalice using parameters=""
-
- 31.5: The precondition at 14.14 might not hold. Insufficient fraction at 14.14 for C.inv. - 67.5: Assertion might not hold. Insufficient fraction at 67.12 for C.value. - 91.5: Assertion might not hold. Insufficient fraction at 91.12 for C.inv. - 95.14: Precondition at 8.14 might not hold. Insufficient fraction at 8.14 for C.inv. - 99.14: Location might not be readable. - 103.28: Precondition at 8.14 might not hold. Insufficient fraction at 8.14 for C.inv. - 107.21: Location might not be readable. - -The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. - 31.5: The statements after the method call statement are unreachable. - 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
diff --git a/Chalice/tests/predicates/test8.chalice b/Chalice/tests/predicates/test8.chalice deleted file mode 100644 index e824f161..00000000 --- a/Chalice/tests/predicates/test8.chalice +++ /dev/null @@ -1,55 +0,0 @@ -// fold/unfold in various combinations
-class FUFU
-{
- var value:int;
- var next:FUFU;
-
- predicate inv { acc(value) }
-
- predicate tinv { acc(value) && acc(next) && (next!=null ==> next.tinv) }
-
- function get():int
- requires tinv;
- { unfolding tinv in value }
-
- method fufu()
- requires acc(value);
- {
- fold inv;
- unfold inv;
- fold inv;
- unfold inv;
- }
-
- method fuf()
- requires acc(value);
- {
- fold inv;
- unfold inv;
- fold inv;
- }
-
- method uf()
- requires inv;
- {
- unfold inv;
- fold inv;
- }
-
- method fu()
- requires acc(value);
- {
- fold inv;
- unfold inv;
- }
-
- method t()
- requires tinv && unfolding tinv in next!=null;
- ensures tinv && unfolding tinv in next!=null;
- {
- unfold tinv;
- unfold next.tinv;
- fold next.tinv;
- fold tinv;
- }
-}
\ No newline at end of file diff --git a/Chalice/tests/predicates/test8.output.txt b/Chalice/tests/predicates/test8.output.txt deleted file mode 100644 index 567d2894..00000000 --- a/Chalice/tests/predicates/test8.output.txt +++ /dev/null @@ -1,4 +0,0 @@ -Verification of test8.chalice using parameters=""
-
- -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 deleted file mode 100644 index 6b276a04..00000000 --- a/Chalice/tests/predicates/unfolding.chalice +++ /dev/null @@ -1,32 +0,0 @@ -class Cell {
- var value: int;
-
- predicate p { acc(value) }
-
- method test()
- requires p
- {
- var tmp: int := unfolding p in value;
- var tmp2: int := unfolding p in value;
- call void()
- assert tmp == unfolding p in value // ERROR: should fail
- }
-
- method test2()
- requires p
- ensures p
- {
- var tmp: int := unfolding p in value;
- var tmp2: int := unfolding p in value;
- call v()
- assert tmp == unfolding p in value
- }
-
- method v() requires true {}
-
- method void()
- requires p
- ensures p
- {}
-
-}
diff --git a/Chalice/tests/predicates/unfolding.output.txt b/Chalice/tests/predicates/unfolding.output.txt deleted file mode 100644 index 7ff49106..00000000 --- a/Chalice/tests/predicates/unfolding.output.txt +++ /dev/null @@ -1,5 +0,0 @@ -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
|