diff options
| author |  stefanheule <unknown> | 2011-08-03 12:14:12 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-08-03 12:14:12 +0200 |
| commit | 291b302fcf1c64c7ef34e7c379d5bffbdd693c5c (patch) | |
| tree | 5403179f83b350f42c7de74dfb31791e1b97978d /Chalice/tests/examples | |
| parent | 80c0bd8588517ff286ec3188e124b9cd5d1b0eed (diff) | |
Chalice: Add regression tests for all fixed bugs and separate the tests in 'examples' into "read" examples and general tests.
Diffstat (limited to 'Chalice/tests/examples')
26 files changed, 1 insertions, 1720 deletions
diff --git a/Chalice/tests/examples/ImplicitLocals.chalice b/Chalice/tests/examples/ImplicitLocals.chalice deleted file mode 100644 index 15ebe8e0..00000000 --- a/Chalice/tests/examples/ImplicitLocals.chalice +++ /dev/null @@ -1,27 +0,0 @@ -class C {
- var k: int;
-
- method MyMethod() returns (x: int, y: C)
- requires acc(k)
- ensures acc(y.k) && x < y.k
- {
- x := k - 15;
- y := this;
- }
-
- method B() {
- var c := new C;
- call a, b := c.MyMethod();
- assert a < b.k;
- }
-
- method D() {
- var ch := new Ch;
- var c := new C;
- send ch(c.k - 15, c); // give ourselves some credit
- receive a, b := ch;
- assert a < b.k;
- }
-}
-
-channel Ch(x: int, y: C) where acc(y.k) && x < y.k;
diff --git a/Chalice/tests/examples/ImplicitLocals.output.txt b/Chalice/tests/examples/ImplicitLocals.output.txt deleted file mode 100644 index db26bba6..00000000 --- a/Chalice/tests/examples/ImplicitLocals.output.txt +++ /dev/null @@ -1,4 +0,0 @@ -Verification of ImplicitLocals.chalice using parameters=""
-
- -Boogie program verifier finished with 0 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/examples/LoopLockChange.chalice b/Chalice/tests/examples/LoopLockChange.chalice deleted file mode 100644 index 5ccce089..00000000 --- a/Chalice/tests/examples/LoopLockChange.chalice +++ /dev/null @@ -1,142 +0,0 @@ -class LoopLockChange { - - method Test0() - requires rd(mu) && waitlevel << mu - lockchange this; - { - acquire this; - - var b := true; - while(b) // error: lockchange clause of loop must include all lock changes that happened before the loop - { - b := false; - } - } - - method Test1() - requires rd(mu) && waitlevel << mu - lockchange this; - { - acquire this; - - var b := true; - while(b) - lockchange this; - { - b := false; - } - } - - method Test2() - requires rd(mu) && waitlevel << mu - lockchange this; - { - var b := true; - while(b) // error: insufficient lockchange clause - invariant rd(mu); - invariant b ==> waitlevel << mu - { - acquire this; - b := false; - } - } - - method Test3() - requires rd(mu) && waitlevel << mu - lockchange this; - { - var b := true; - while(b) - invariant rd(mu); - invariant b ==> waitlevel << mu - lockchange this; - { - acquire this; - b := false; - } - } - - method Test4(p: LoopLockChange) - requires rd(p.mu) && waitlevel << p.mu - requires rd(mu) && waitlevel << mu - { - var current: LoopLockChange := this; - var b := true; - while(b) - invariant rd(current.mu) - invariant b ==> rd(p.mu); - invariant b ==> waitlevel << current.mu - lockchange current; // error: after the loop body, current does no longer point to the object whose lock was acquired - { - acquire current; - current := p; - b := false; - } - assume false; // to prevent complaint about method's lockchange clause - } - - - method Test5(p: LoopLockChange) - requires rd(p.mu) && waitlevel << p.mu - requires rd(mu) && waitlevel << mu - lockchange this; - { - var current: LoopLockChange := this; - var b := true; - while(b) - invariant rd(current.mu) - invariant b ==> rd(p.mu); - invariant b ==> current == this; - invariant b ==> waitlevel << current.mu - lockchange this; - { - acquire current; - current := p; - b := false; - } - } - - - method Test6() - requires rd(mu) && waitlevel << mu - { - var b := true; - while(b) - invariant rd(mu); - invariant b ==> waitlevel << mu - invariant b ==> !(rd holds(this)) - invariant !b ==> holds(this) - lockchange this; - { - acquire this; - b := false; - } - release this; - } - - - method Test7() - requires rd(mu) && waitlevel << mu - { - acquire this; - release this; - } - - -// The following test requires a better treatment of allocation, which we don't have yet -/* method Test8() - { - var tmp : LoopLockChange := this; - var b := false; - while(b) - { - tmp := new LoopLockChange; - share tmp; - acquire tmp; - b := false; - } - assert !holds(tmp); - } -*/ -} - diff --git a/Chalice/tests/examples/LoopLockChange.output.txt b/Chalice/tests/examples/LoopLockChange.output.txt deleted file mode 100644 index 19e84f93..00000000 --- a/Chalice/tests/examples/LoopLockChange.output.txt +++ /dev/null @@ -1,12 +0,0 @@ -Verification of LoopLockChange.chalice using parameters=""
-
- 10.5: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop. - 35.5: The loop might lock/unlock more than the lockchange clause allows. - 65.5: The loop might lock/unlock more than the lockchange clause allows. - -The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. - 10.5: The begging of the while-body is unreachable. - 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.
diff --git a/Chalice/tests/examples/ProdConsChannel.chalice b/Chalice/tests/examples/ProdConsChannel.chalice index 563d72b6..abac4f5c 100644 --- a/Chalice/tests/examples/ProdConsChannel.chalice +++ b/Chalice/tests/examples/ProdConsChannel.chalice @@ -42,85 +42,4 @@ class Program { receive c := ch
}
}
-
- // variations
- method Main0() { // error: debt remains after body
- var ch := new Ch
- fork tk0 := Producer(ch)
- fork tk1 := Consumer(ch)
- // join tk0
- join tk1
- }
- method Main1() {
- var ch := new Ch
- fork tk0 := Producer(ch)
- fork tk1 := Consumer(ch)
- join tk0
- // join tk1
- } // no problem
- method Producer0(ch: Ch) // error: debt remains after body
- requires ch != null
- ensures credit(ch)
- {
- var i := 0
- while (i < 25)
- {
- var x := i*i
- var c := new Cell { val := x }
- send ch(c)
- i := i + 1
- }
- // send ch(null)
- }
- method Producer1(ch: Ch)
- requires ch != null
- ensures credit(ch)
- {
- var i := 0
- while (i < 25)
- {
- var x := i*i
- var c := new Cell { val := x }
- send ch(c)
- i := i + 1 + c.val // error: can no longer read c.val
- }
- send ch(null)
- }
- method Consumer0(ch: Ch)
- requires rd(ch.mu) && waitlevel << ch.mu
- requires credit(ch)
- ensures rd(ch.mu)
- {
- var c: Cell
- receive c := ch
- while (c != null && c.val == 7) // this consumer may end early, but that's allowed
- invariant rd(ch.mu) && waitlevel << ch.mu
- invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)
- {
- var i := c.val
- receive c := ch
- }
- }
- method Consumer1(ch: Ch)
- requires rd(ch.mu) && waitlevel << ch.mu
- requires credit(ch)
- ensures rd(ch.mu)
- {
- var c: Cell
- receive c := ch
- if (c != null) {
- assert 0 <= c.val // follows from where clause
- }
- }
- method Consumer2(ch: Ch)
- requires rd(ch.mu) && waitlevel << ch.mu
- requires credit(ch)
- ensures rd(ch.mu)
- {
- var c: Cell
- receive c := ch
- if (c != null) {
- assert c.val < 2 // error: does not follow from where clause
- }
- }
}
diff --git a/Chalice/tests/examples/ProdConsChannel.output.txt b/Chalice/tests/examples/ProdConsChannel.output.txt index 167898fb..4d91605c 100644 --- a/Chalice/tests/examples/ProdConsChannel.output.txt +++ b/Chalice/tests/examples/ProdConsChannel.output.txt @@ -1,11 +1,4 @@ Verification of ProdConsChannel.chalice using parameters=""
- 47.3: Method body is not allowed to leave any debt. - 61.3: Method body is not allowed to leave any debt. - 85.20: Location might not be readable. - 123.7: Assertion might not hold. The expression at 123.14 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. - 80.5: The end of the while-loop is unreachable. - -Boogie program verifier finished with 4 errors and 1 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/examples/RockBand-automagic.chalice b/Chalice/tests/examples/RockBand-automagic.chalice deleted file mode 100644 index 8a64b691..00000000 --- a/Chalice/tests/examples/RockBand-automagic.chalice +++ /dev/null @@ -1,112 +0,0 @@ -// chalice-parameter=-checkLeaks -defaults -autoFold -autoMagic
-// verify this program with -checkLeaks -defaults -autoFold -autoMagic
-
-class Client {
- method Main() {
- var b := new RockBand
- call b.Init()
- call b.Play()
- call b.Play()
- call b.Dispose()
- }
-}
-
-class RockBand module M {
- var gigs: int
- var gt: Guitar
- var doowops: seq<Vocalist>
- var b3: Organ
- predicate Valid {
- /*acc(gigs) &&*/ 0 <= gigs &&
- /*acc(gt) && gt != null &&*/ gt.Valid &&
- acc(gt.mu) &&
- acc(doowops) &&
- /*acc(b3) && b3 != null &&*/ b3.Valid &&
- acc(b3.mu)
- }
-
- method Init()
- requires acc(this.*)
- ensures Valid
- {
- gigs := 0
- gt := new Guitar
- call gt.Init()
- b3 := new Organ
- call b3.Init()
- }
-
- method Dispose()
- requires Valid && acc(mu)
- {
- call gt.Dispose()
- call b3.Dispose()
- free this
- }
-
- method Play()
- requires Valid
- ensures Valid
- {
- gigs := gigs + 1
- call gt.Strum()
- call b3.Grind()
- }
-}
-
-class Guitar module Musicians {
- predicate Valid { true }
- method Init()
- requires acc(this.*)
- ensures Valid
- {
- }
- method Dispose()
- requires Valid && acc(mu)
- {
- free this
- }
- method Strum()
- requires Valid
- ensures Valid
- {
- }
-}
-
-class Vocalist module Musicians {
- predicate Valid { true }
- method Init()
- requires acc(this.*)
- ensures Valid
- {
- }
- method Dispose()
- requires Valid && acc(mu)
- {
- free this
- }
- method Strum()
- requires Valid
- ensures Valid
- {
- }
-}
-
-class Organ module Musicians {
- predicate Valid { true }
- method Init()
- requires acc(this.*)
- ensures Valid
- {
- }
- method Dispose()
- requires Valid && acc(mu)
- {
- free this
- }
- method Grind()
- requires Valid
- ensures Valid
- {
- }
-}
diff --git a/Chalice/tests/examples/RockBand-automagic.output.txt b/Chalice/tests/examples/RockBand-automagic.output.txt deleted file mode 100644 index 2e62b457..00000000 --- a/Chalice/tests/examples/RockBand-automagic.output.txt +++ /dev/null @@ -1,4 +0,0 @@ -Verification of RockBand-automagic.chalice using parameters="-checkLeaks -defaults -autoFold -autoMagic"
-
- -Boogie program verifier finished with 0 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/examples/SmokeTestTest.chalice b/Chalice/tests/examples/SmokeTestTest.chalice deleted file mode 100644 index 6ff283ec..00000000 --- a/Chalice/tests/examples/SmokeTestTest.chalice +++ /dev/null @@ -1,121 +0,0 @@ -// This file is meant as a test for Chalice's smoke testing feature (command line switch -smoke)
-class Cell {
- var f: int;
-
- invariant acc(this.f) && f == 1
- invariant f == 2 // SMOKE: contradiction
-
- method a1()
- requires false // SMOKE: precondition is false
- {}
-
- method a2()
- requires acc(this.f,-2) // SMOKE: precondition is equivalent to false
- {}
-
- method a3()
- requires acc(this.f)
- {
- if (this.f > 0) {
- this.f := 0;
- }
- }
-
- method a4()
- requires acc(this.f)
- {
- if (false) {
- this.f := 0; // SMOKE: unreachable
- }
- }
-
- method a5()
- requires acc(this.f)
- {
- if (true) {
- this.f := 0;
- }
- }
-
- method a6()
- requires acc(this.f)
- {
- if (false) {
- this.f := 0; // SMOKE: unreachable
- } else {
- this.f := 1;
- }
- }
-
- method a7(i: int, j: int)
- requires i != j;
- {
- assume i == j; // SMOKE: introduces contradiction
- }
-
- method a8()
- requires acc(this.f)
- {
- while (true)
- invariant acc(this.f)
- {
- this.f := this.f + 1
- }
- // SMOKE: unreachable, loop does not terminate
- }
-
- method a9()
- requires acc(this.f)
- {
- call a8()
- }
-
- method a10()
- requires acc(this.f)
- {
- if (true) {
- this.f := 0;
- } else {
- this.f := 1; // SMOKE: unreachable
- }
- }
-
- function f1(): int
- requires false // SMOKE: precondition is false
- { 1 }
-
- method a11()
- {
- var i: int := 0
- if (false) {
- // SMOKE: unreachable
- } else {
- if (true) { assume false } // SMOKE: introduces contradiction
- else { assume i == 1 } // SMOKE: introduces contradiction
- }
- }
-
- method a12()
- {
- assume false // SMOKE: introduces contradiction
- while (false) {
-
- }
- }
-
- method a13()
- ensures false // ERROR: cannot prove false
- {
- }
-
- method a14()
- {
- call a13(); // SMOKE: statements afterwards not reachable anymore
- }
-
- predicate valid {
- 1 == 2 // SMOKE: contradiction
- }
-}
-
-channel C(msg: bool) where msg && !msg // SMOKE: contradiction
\ No newline at end of file diff --git a/Chalice/tests/examples/SmokeTestTest.output.txt b/Chalice/tests/examples/SmokeTestTest.output.txt deleted file mode 100644 index 3d1cd786..00000000 --- a/Chalice/tests/examples/SmokeTestTest.output.txt +++ /dev/null @@ -1,23 +0,0 @@ -Verification of SmokeTestTest.chalice using parameters=""
-
- 106.3: The postcondition at 107.13 might not hold. The expression at 107.13 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. - 2.1: Monitor invariant is equivalent to false. - 8.3: Precondition of method a1 is equivalent to false. - 12.3: Precondition of method a2 is equivalent to false. - 27.5: The begging of the if-branch is unreachable. - 43.5: The begging of the if-branch is unreachable. - 53.5: Assumption introduces a contradiction. - 59.5: The statements after the while-loop are unreachable. - 76.5: The begging of the else-branch is unreachable. - 83.3: Precondition of function f1 is equivalent to false. - 90.5: The begging of the if-branch is unreachable. - 93.7: The begging of the else-branch is unreachable. - 93.19: Assumption introduces a contradiction. - 100.5: Assumption introduces a contradiction. - 113.5: The statements after the method call statement are unreachable. - 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.
diff --git a/Chalice/tests/examples/cell-defaults.chalice b/Chalice/tests/examples/cell-defaults.chalice deleted file mode 100644 index eb826f89..00000000 --- a/Chalice/tests/examples/cell-defaults.chalice +++ /dev/null @@ -1,153 +0,0 @@ -// chalice-parameter=-defaults -autoFold -autoMagic
-// verify this program with -defaults -autoFold -autoMagic
-
-class Cell module Library {
- var x: int;
-
- method init(v: int)
- requires acc(this.x) && 0<=v;
- ensures valid && this.get() == v;
- {
- x := v;
- }
-
- method set(v: int)
- requires valid && 0<=v;
- ensures valid && get()==v;
- {
- x := v;
- }
-
- method increment()
- requires valid;
- ensures valid && get() == old(get()) + 1;
- {
- x := x + 1;
- }
-
- method dispose()
- requires valid && acc(mu);
- ensures true;
- {
- free this;
- }
-
- function get(): int
- requires valid;
- ensures 0<=result;
- {
- x
- }
-
- predicate valid {
- acc(this.x) && 0<=x
- }
-
- invariant valid;
-}
-
-class Interval module Library2 {
- var left: Cell;
- var right: Cell;
-
- method init(l: int, r: int)
- requires 0<=l && l <= r;
- requires acc(left) && acc(right);
- ensures valid;
- ensures getLeft()==l
- ensures getRight()==r;
- {
- left := new Cell;
- call left.init(l);
- right := new Cell;
- call right.init(r);
- }
-
- method setLeft(l: int)
- requires valid;
- requires 0<=l && l<=getRight();
- ensures valid;
- ensures getLeft()==l && getRight()==old(getRight());
- {
- call left.set(l);
- }
-
- method setRight(r: int)
- requires valid;
- requires 0<=r && getLeft()<=r;
- ensures valid;
- ensures getLeft()==old(getLeft()) && getRight()==r;
- {
- call right.set(r);
- }
-
- method shift(v: int)
- requires valid;
- requires 0<=v;
- ensures valid;
- ensures getLeft()==old(getLeft())+v && getRight()==old(getRight())+v;
- {
- call left.set(left.get()+v);
- call right.set(right.get()+v);
- }
-
- function getLeft() : int
- requires valid;
- {
- left.get() // for some reason, Boogie can't figure out the callee's heap is smaller when using defaults
- }
-
- function getRight() : int
- requires valid;
- {
- right.get() // for some reason, Boogie can't figure out the callee's heap is smaller when using defaults
- }
-
- predicate valid
- {
- left.valid && right.valid && left.get() <= right.get()
- }
-}
-
-class Program module Main {
- method main(){
- var c1 := new Cell;
- call c1.init(5);
- call c1.set(6);
-
- var c2 := new Cell;
- call c2.init(10);
- call c2.set(11);
-
- assert c1.get() == 6;
- }
-
- method main2(){
- var c: Cell;
-
- c := new Cell;
- call c.init(0);
- call c.dispose();
-
- assert c.valid; // should fail
- }
-
- method main3() returns (rt: Cell)
- ensures rt!=null && rt.valid && rt.get() == 0
- {
- rt := new Cell;
- call rt.init(0)
- }
-
- method main4() {
- var c: Cell;
-
- c := new Cell;
- call c.init(0);
- share c;
-
- acquire c;
- call c.set(1);
- release c;
- }
-}
\ No newline at end of file diff --git a/Chalice/tests/examples/cell-defaults.output.txt b/Chalice/tests/examples/cell-defaults.output.txt deleted file mode 100644 index 138a5717..00000000 --- a/Chalice/tests/examples/cell-defaults.output.txt +++ /dev/null @@ -1,10 +0,0 @@ -Verification of cell-defaults.chalice using parameters="-defaults -autoFold -autoMagic"
-
- 97.5: The heap of the callee might not be strictly smaller than the heap of the caller. - 103.5: The heap of the callee might not be strictly smaller than the heap of the caller. - 132.5: Assertion might not hold. Insufficient fraction at 132.12 for Cell.valid. - -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.
diff --git a/Chalice/tests/examples/counter.chalice b/Chalice/tests/examples/counter.chalice deleted file mode 100644 index 828cf005..00000000 --- a/Chalice/tests/examples/counter.chalice +++ /dev/null @@ -1,152 +0,0 @@ -class Counter {
- var value: int;
-
- invariant acc(value) && old(value)<=value;
-}
-
-class Program {
-
- method main1(){
- var counter := new Counter;
- counter.value := 0;
- share counter;
-
- acquire counter;
- var tmp1 := counter.value;
- release counter;
-
- acquire counter;
- var tmp2 := counter.value;
- release counter;
-
- assert tmp1 <= tmp2;
- }
-
- method main2(){
- var counter := new Counter;
- counter.value := 0;
- share counter;
-
- acquire counter;
- release counter;
-
- call bar(counter);
- }
-
- method bar(c: Counter)
- requires c!=null && acc(c.mu) && waitlevel << c.mu;
- requires eval(c.release, acc(c.value) && 0<=c.value);
- {
- lock (c) {
- assert 0 <= c.value; // ok, because of the lastSeen conjunct in the precondition
- }
- }
-
- method main3() returns (counter: Counter)
- lockchange counter;
- {
- counter := new Counter;
- counter.value := 0;
- share counter;
- acquire counter;
- call doRelease(counter, counter.value);
- }
-
- method doRelease(c: Counter, i: int)
- requires c!=null && holds(c) && acc(c.value) && eval(c.acquire, acc(c.value) && i<=c.value);
- lockchange c;
- {
- release c; // ok, because of atAcquire conjunct in the precondition
- }
-
- method main4(){
- var counter := new Counter;
- counter.value := 0;
- share counter;
-
- acquire counter;
- counter.value := counter.value - 1;
- release counter; // error: should fail
- }
-
- method main5(){
- var counter := new Counter;
- counter.value := 10;
- share counter;
-
- call foo(counter);
-
- unshare counter;
- assert 10<=counter.value; // error: should fail
- }
-
- method foo(c: Counter)
- requires c!=null && acc(c.mu) && waitlevel << c.mu && eval(c.release, acc(c.value) && 10<=c.value);
- ensures c!=null && holds(c) && acc(c.mu) && acc(c.value);
- lockchange c;
- {
- acquire c;
- unshare c;
- c.value := 5;
- share c;
- acquire c;
- }
-
- method nestedGood0(c: Counter)
- requires c != null && acc(c.mu) && waitlevel << c.mu;
- {
- lock (c) {
- release c
- acquire c
- }
- }
-
- method nestedGood1(c: Counter)
- requires c != null && acc(c.mu) && waitlevel << c.mu;
- {
- var t: Counter := c
- lock (t) {
- t := new Counter
- share t
- acquire t
- } // this line releases the original value for t
- release t
- }
-
- method nestedBad0(c: Counter)
- requires c != null && acc(c.mu) && waitlevel << c.mu;
- {
- lock (c) {
- release c
- } // error: no longer holds c
- }
-
- method nestedBad1(c: Counter)
- requires c != null && acc(c.mu) && waitlevel << c.mu;
- {
- lock (c) {
- acquire c // error: already holds c
- }
- }
-
- method nestedBad2(c: Counter)
- requires c != null && acc(c.mu) && waitlevel << c.mu;
- {
- lock (c) {
- lock (c) { // error: already holds c
- }
- }
- }
-
- method nestedBad3(c: Counter)
- requires c != null && acc(c.mu) && waitlevel << c.mu;
- {
- var t: Counter := c
- lock (t) {
- release t
- t := new Counter
- share t
- acquire t
- } // error: this line attempts to release the original t
- }
-}
\ No newline at end of file diff --git a/Chalice/tests/examples/counter.output.txt b/Chalice/tests/examples/counter.output.txt deleted file mode 100644 index 1d5be0ea..00000000 --- a/Chalice/tests/examples/counter.output.txt +++ /dev/null @@ -1,17 +0,0 @@ -Verification of counter.chalice using parameters=""
-
- 69.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true. - 80.5: Assertion might not hold. The expression at 80.12 might not evaluate to true. - 119.5: The target of the release statement might not be locked by the current thread. - 128.7: The mu field of the target of the acquire statement might not be above waitlevel. - 136.7: The mu field of the target of the acquire statement might not be above waitlevel. - 145.5: The target of the release statement might not be locked by the current thread. - -The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. - 62.3: The end of method main4 is unreachable. - 116.3: The end of method nestedBad0 is unreachable. - 128.7: The statements after the acquire statement are unreachable. - 136.7: The begging of the lock-block is unreachable. - 141.3: The end of method nestedBad3 is unreachable. - -Boogie program verifier finished with 6 errors and 5 smoke test warnings.
diff --git a/Chalice/tests/examples/prog0.chalice b/Chalice/tests/examples/prog0.chalice deleted file mode 100644 index fb835a24..00000000 --- a/Chalice/tests/examples/prog0.chalice +++ /dev/null @@ -1,109 +0,0 @@ -class C {
- method m() {
- assert 4 + (a * 5) + (2 + 3) * (a + a);
- a := a + 3;
- b := a - b - c + 4 * d + 20 + --25;
- b := ((((a - b) - c) + 4 * d) + 20) + --25;
- c := a - (b - (c + (4 * d + (20 + 25))));
- assert (X ==> Y) ==> Z <==> A ==> B ==> C;
- assume A && B && (C || D || E) && F;
- var x;
- var y := 12 + !(x.f.g).h - (!x).f + (!x.f);
- var z := new C;
- y := new D;
- o.f := 5;
- (a + b).y := new T;
- reorder (2 ==(O != 3)) != O between a,b,c and x,y,z;
- reorder X ==> Y below x+5;
- reorder o.f above this, null;
- share o;
- unshare o;
- acquire o;
- release o;
- rd acquire o;
- rd release o;
- downgrade o;
- var tok: token<C.m>;
- fork tok := o.m();
- join tok;
- assert rd(x) + acc(y) + acc(z, 1/4) + old(old(k)) + null.f;
- x := this.f;
- call m(2,3,4);
- call this.m(2,3,4);
- call a,b,c := o.m();
- call x := m(200);
- reorder o above waitlevel;
- }
- method p(a,b,c) returns (x,y,z)
- requires 8 + 2 == 10;
- ensures 8 + 5 > 10;
- requires x == y+1;
- ensures old(x) < x;
- {
- if (x == 7) {
- y := y + 1; z := z + 2;
- } else if (x == 8) {
- y := 2;
- } else {
- z := 10;
- }
- { // empty block
- }
- if (x == 9) { }
- if (x == 10) { x := 10; } else { }
- var n := 0;
- while (n < 100) { n := n - 1; }
- while (n != 0)
- invariant n % 2 == 0;
- invariant sqrt2 * sqrt2 == 2;
- {
- n := n - 2;
- }
- call v,x := s.M(65);
- }
-}
-class D { }
-
-// ----- tests specifically of implicit locals in CALL and RECEIVE statements
-
-class ImplicitC {
- var k: int;
-
- method MyMethod() returns (x: int, y: ImplicitC)
- requires acc(k)
- ensures acc(y.k) && x < y.k
- {
- x := k - 15;
- y := this;
- }
-
- method B0() {
- var c := new ImplicitC;
- call a, b := c.MyMethodX(); // error: method not found (so what is done with a,b?)
- assert a < b.k;
- }
-
- method B1() {
- var c := new ImplicitC;
- call a, a := c.MyMethod(); // error: a occurs twice
- assert a < b.k;
- }
-
- method D0() {
- var ch := new Ch;
- var c := new ImplicitC;
- send ch(c.k - 15, c); // give ourselves some credit
- receive a, b := chX; // error: channel not found (so what is done with a,b?)
- assert a < b.k;
- }
-
- method D1() {
- var ch := new Ch;
- var c := new ImplicitC;
- send ch(c.k - 15, c); // give ourselves some credit
- receive a, a := ch; // error: a occurs twice
- assert a < b.k;
- }
-}
-
-channel Ch(x: int, y: ImplicitC) where acc(y.k) && x < y.k;
diff --git a/Chalice/tests/examples/prog0.output.txt b/Chalice/tests/examples/prog0.output.txt deleted file mode 100644 index 5b329874..00000000 --- a/Chalice/tests/examples/prog0.output.txt +++ /dev/null @@ -1,146 +0,0 @@ -Verification of prog0.chalice using parameters=""
-
-The program did not typecheck.
-3.17: undeclared member a in class C
-3.37: undeclared member a in class C
-3.41: undeclared member a in class C
-3.12: assert statement requires a boolean expression (found int)
-4.5: undeclared member a in class C
-4.10: undeclared member a in class C
-5.5: undeclared member b in class C
-5.10: undeclared member a in class C
-5.14: undeclared member b in class C
-5.18: undeclared member c in class C
-5.26: undeclared member d in class C
-6.5: undeclared member b in class C
-6.14: undeclared member a in class C
-6.18: undeclared member b in class C
-6.23: undeclared member c in class C
-6.32: undeclared member d in class C
-7.5: undeclared member c in class C
-7.10: undeclared member a in class C
-7.15: undeclared member b in class C
-7.20: undeclared member c in class C
-7.29: undeclared member d in class C
-8.13: undeclared member X in class C
-8.19: undeclared member Y in class C
-8.13: incorrect type of ==> LHS (expected bool, found int)
-8.19: incorrect type of ==> RHS (expected bool, found int)
-8.26: undeclared member Z in class C
-8.26: incorrect type of ==> RHS (expected bool, found int)
-8.33: undeclared member A in class C
-8.39: undeclared member B in class C
-8.45: undeclared member C in class C
-8.39: incorrect type of ==> LHS (expected bool, found int)
-8.45: incorrect type of ==> RHS (expected bool, found int)
-8.33: incorrect type of ==> LHS (expected bool, found int)
-9.12: undeclared member A in class C
-9.17: undeclared member B in class C
-9.12: incorrect type of && LHS (expected bool, found int)
-9.17: incorrect type of && RHS (expected bool, found int)
-9.23: undeclared member C in class C
-9.28: undeclared member D in class C
-9.23: incorrect type of || LHS (expected bool, found int)
-9.28: incorrect type of || RHS (expected bool, found int)
-9.33: undeclared member E in class C
-9.33: incorrect type of || RHS (expected bool, found int)
-9.39: undeclared member F in class C
-9.39: incorrect type of && RHS (expected bool, found int)
-11.21: undeclared member f in class int
-11.21: undeclared member g in class int
-11.21: undeclared member h in class int
-<undefined position>: not-expression requires boolean operand
-<undefined position>: incorrect type of + RHS (expected int, found bool)
-11.33: not-expression requires boolean operand
-11.33: undeclared member f in class bool
-11.43: undeclared member f in class int
-11.42: not-expression requires boolean operand
-11.42: incorrect type of + RHS (expected int, found bool)
-13.5: type mismatch in assignment, lhs=int rhs=D
-14.5: undeclared member o in class C
-14.5: undeclared member f in class int
-15.6: undeclared member a in class C
-15.10: undeclared member b in class C
-15.5: undeclared member y in class int
-15.18: undefined class or channel T used in new expression
-16.19: undeclared member O in class C
-16.14: == requires operands of the same type, found int and bool
-16.31: undeclared member O in class C
-16.13: != requires operands of the same type, found bool and int
-16.13: object in reorder statement must be of a reference type (found bool)
-16.41: undeclared member a in class C
-16.41: install bound must be of a reference type or Mu type (found int)
-16.43: undeclared member b in class C
-16.43: install bound must be of a reference type or Mu type (found int)
-16.45: undeclared member c in class C
-16.45: install bound must be of a reference type or Mu type (found int)
-16.51: install bound must be of a reference type or Mu type (found int)
-16.53: install bound must be of a reference type or Mu type (found int)
-17.13: undeclared member X in class C
-17.19: undeclared member Y in class C
-17.13: incorrect type of ==> LHS (expected bool, found int)
-17.19: incorrect type of ==> RHS (expected bool, found int)
-17.13: object in reorder statement must be of a reference type (found bool)
-17.27: install bound must be of a reference type or Mu type (found int)
-18.13: undeclared member o in class C
-18.13: undeclared member f in class int
-18.13: object in reorder statement must be of a reference type (found int)
-19.11: undeclared member o in class C
-19.11: object in share statement must be of a reference type (found int)
-20.13: undeclared member o in class C
-20.13: object in unshare statement must be of a reference type (found int)
-21.13: undeclared member o in class C
-21.13: object in acquire statement must be of a reference type (found int)
-22.13: undeclared member o in class C
-22.13: object in release statement must be of a reference type (found int)
-23.16: undeclared member o in class C
-23.16: object in rd acquire statement must be of a reference type (found int)
-24.16: undeclared member o in class C
-24.16: object in rd release statement must be of a reference type (found int)
-25.15: undeclared member o in class C
-25.15: object in downgrade statement must be of a reference type (found int)
-27.17: undeclared member o in class C
-27.5: call of undeclared member m in class int
-27.10: wrong token type
-29.12: rd expression is allowed only in positive predicate contexts
-29.15: undeclared member x in class C
-29.20: acc expression is allowed only in positive predicate contexts
-29.24: undeclared member y in class C
-29.12: incorrect type of + LHS (expected int, found bool)
-29.20: incorrect type of + RHS (expected int, found bool)
-29.29: acc expression is allowed only in positive predicate contexts
-29.33: undeclared member z in class C
-29.29: incorrect type of + RHS (expected int, found bool)
-29.51: undeclared member k in class C
-29.57: undeclared member f in class null
-29.12: assert statement requires a boolean expression (found int)
-30.10: undeclared member f in class C
-31.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)
-32.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)
-33.19: undeclared member o in class C
-33.5: call of undeclared member m in class int
-34.5: wrong number of actual in-parameters in call to C.m (1 instead of 0)
-34.5: wrong number of actual out-parameters in call to C.m (1 instead of 0)
-35.13: undeclared member o in class C
-35.13: object in reorder statement must be of a reference type (found int)
-58.17: undeclared member sqrt2 in class C
-58.25: undeclared member sqrt2 in class C
-62.17: undeclared member s in class C
-62.5: call of undeclared member M in class int
-82.5: call of undeclared member MyMethodX in class ImplicitC
-83.12: undefined local variable a
-83.16: undefined local variable b
-83.16: undeclared member k in class int
-88.13: the type of the formal argument is not assignable to the actual parameter (expected: ImplicitC, found: int)
-88.13: duplicate actual out-parameter: a
-89.16: undeclared member b in class ImplicitC
-89.16: undeclared member k in class int
-96.21: undeclared member chX in class ImplicitC
-96.5: receive expression (which has type int) does not denote a channel
-97.12: undefined local variable a
-97.16: undefined local variable b
-97.16: undeclared member k in class int
-104.16: the type of the formal argument is not assignable to the actual parameter (expected: ImplicitC, found: int)
-104.16: duplicate actual out-parameter: a
-105.16: undeclared member b in class ImplicitC
-105.16: undeclared member k in class int
diff --git a/Chalice/tests/examples/prog1.chalice b/Chalice/tests/examples/prog1.chalice deleted file mode 100644 index 133de36d..00000000 --- a/Chalice/tests/examples/prog1.chalice +++ /dev/null @@ -1,86 +0,0 @@ -// 7 errors expected
-
-class C {
- var x: int;
- invariant acc(x) && 0 <= x;
-
- method seq0() returns (r: int)
- {
- r := x; // error: cannot access this.x here (90)
- }
- method seq1() returns (r: int)
- requires acc(x);
- {
- r := x;
- }
- method seq2() returns (r: int)
- requires rd(x);
- {
- r := x;
- }
- method seq3() returns (r: int)
- requires rd(x);
- {
- r := x;
- x := x + 1; // error: cannot write to this.x here (184)
- }
-
- method main0()
- {
- var c := new C;
- c.x := 0;
- share c;
- var t := c.x; // error: cannot access c.x now (254)
- }
- method main1()
- {
- var c := new C;
- c.x := 2;
- share c;
- acquire c;
- c.x := c.x - 1;
- release c; // error: monitor invariant might not hold (362)
- }
- method main2()
- {
- var c := new C;
- c.x := 2;
- share c;
- acquire c;
- c.x := c.x + 1;
- release c; // good!
- }
- method main3()
- {
- var c := new C;
- c.x := 2;
- share c;
- rd acquire c;
- var tmp := c.x + 1; // fine
- c.x := tmp; // error: cannot write to c.x here (582)
- rd release c;
- }
- method main4()
- {
- var c := new C;
- c.x := 2;
- share c;
- acquire c;
- c.x := c.x + 1;
- unshare c;
- c.x := c.x + 1;
- }
- method main5()
- {
- var c := new C;
- unshare c; // error: cannot unshare an object that isn't shared (754)
- }
- method main6()
- {
- var c := new C;
- c.x := 0;
- share c; acquire c;
- unshare c;
- unshare c; // error: cannot unshare an object that isn't shared (862)
- }
-}
\ No newline at end of file diff --git a/Chalice/tests/examples/prog1.output.txt b/Chalice/tests/examples/prog1.output.txt deleted file mode 100644 index 630ecdfa..00000000 --- a/Chalice/tests/examples/prog1.output.txt +++ /dev/null @@ -1,19 +0,0 @@ -Verification of prog1.chalice using parameters=""
-
- 9.10: Location might not be readable. - 25.5: Location might not be writable - 33.14: Location might not be readable. - 42.5: Monitor invariant might hot hold. The expression at 5.23 might not evaluate to true. - 60.5: Location might not be writable - 76.5: The target of the unshare statement might not be shared. - 84.5: The target of the unshare statement might not be shared. - -The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. - 7.3: The end of method seq0 is unreachable. - 21.3: The end of method seq3 is unreachable. - 28.3: The end of method main0 is unreachable. - 53.3: The end of method main3 is unreachable. - 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.
diff --git a/Chalice/tests/examples/prog2.chalice b/Chalice/tests/examples/prog2.chalice deleted file mode 100644 index 55fe8ff5..00000000 --- a/Chalice/tests/examples/prog2.chalice +++ /dev/null @@ -1,93 +0,0 @@ -// 4 errors expected
-
-class C {
- method M(x: int) returns (y: bool)
- requires 0 <= x;
- ensures y <==> x == 10;
- {
- y := true;
- if (x != 10) { y := !y; }
- }
-
- method Caller0()
- {
- var b: bool;
- call b := M(12);
- assert !b;
- call b := M(10);
- assert b;
- }
- method Caller1()
- {
- var b: bool;
- call b := M(11);
- assert b; // error (258)
- }
-
- var F: int;
-
- method P(n: int)
- requires acc(F);
- ensures F == old(F) + n; // error
- {
- F := F + n;
- }
- method Caller2()
- requires acc(F);
- {
- var prev := F;
- call P(2);
- assert false; // succeeds because postcondition of P is not well-defined (i.e. we do not havoc this.F, so the verifier assumes the value is the same in pre and post)
- }
-
- method Q(n: int)
- requires acc(F);
- ensures acc(F) && F == old(F) + n;
- {
- F := F + n;
- }
- method Caller3()
- requires acc(F);
- ensures acc(F);
- {
- var prev := F;
- call Q(2);
- assert F == prev + 2;
- }
-}
-
-class Consts {
- method M0() returns (z: int)
- ensures z == 5
- {
- const a := 5
- z := a
- }
- method M1() {
- ghost const a
- a := 5
- }
- method M2() {
- ghost const a
- a := 5
- a := 5 // error (569)
- }
- method M3(b: bool) {
- ghost const a
- if (b) { a := 5 }
- assert a < 10 // error (611)
- }
- method M4(b: bool) {
- ghost const a
- if (b) { a := 5 }
- ghost var x := a
- if (!b) { a := 7 }
- assert a < 10
- assert b ==> x == 5 // cool, huh?
- }
- method M5(b: bool) {
- ghost const a
- if (b) { a := 5 }
- assert assigned(a) ==> a == 5
- }
-}
diff --git a/Chalice/tests/examples/prog2.output.txt b/Chalice/tests/examples/prog2.output.txt deleted file mode 100644 index b9d88bbe..00000000 --- a/Chalice/tests/examples/prog2.output.txt +++ /dev/null @@ -1,13 +0,0 @@ -Verification of prog2.chalice using parameters=""
-
- 24.5: Assertion might not hold. The expression at 24.12 might not evaluate to true. - 31.13: Location might not be readable. - 73.5: Const variable can be assigned to only once. - 78.5: Assertion might not hold. The expression at 78.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. - 20.3: The end of method Caller1 is unreachable. - 39.5: The statements after the method call statement are unreachable. - 70.3: The end of method M2 is unreachable. - -Boogie program verifier finished with 4 errors and 3 smoke test warnings.
diff --git a/Chalice/tests/examples/prog3.chalice b/Chalice/tests/examples/prog3.chalice deleted file mode 100644 index de5dfad7..00000000 --- a/Chalice/tests/examples/prog3.chalice +++ /dev/null @@ -1,246 +0,0 @@ -// 4 errors expected
-
-class Main {
- method A() {
- var d := new Data;
- call d.Init();
- share d;
-
- var t0: T := new T; t0.d := d;
- share t0 between waitlevel and d
- var t1: T := new T; t1.d := d;
- share t1 between waitlevel and d
-
- var t0Token: token<T.run>;
- fork t0Token := t0.run();
- var t1Token: token<T.run>;
- fork t1Token := t1.run();
-
- join t0Token; acquire t0; unshare t0;
- join t1Token; acquire t1; unshare t1;
-
- acquire d; unshare d;
- assert 0 <= d.x && d.x < 100;
- }
-
- method B() returns (r: U)
- lockchange r;
- {
- var u := new U;
- share u;
-
- var uToken: token<U.run>;
- fork uToken := u.run();
-
- acquire u; // a little unusual to acquire after a fork, but allowed
- assert waitlevel == u.mu;
-
- var v := new U;
- share v; acquire v; // this line has the effect of increasing waitlevel
-
- assert waitlevel == v.mu;
- assert waitlevel != u.mu;
- assert u << v;
- assert u << waitlevel;
-
- join uToken; // material for the smoke check
- release u;
- r := v;
- }
-
- method C()
- ensures waitlevel == old(waitlevel);
- {
- var u := new U;
- share u;
- acquire u;
- release u;
- }
-
- method Mx0()
- {
- }
- method Mx1()
- lockchange this
- {
- }
- method MxCaller0()
- ensures waitlevel == old(waitlevel);
- {
- }
- method MxCaller1()
- ensures waitlevel == old(waitlevel);
- {
- call Mx0();
- }
- method MxCaller2()
- ensures waitlevel == old(waitlevel); // error
- {
- call Mx1();
- } // error: missing lockchange
-
- method D(u: U)
- requires u != null && rd(u.mu) && waitlevel << u;
- ensures waitlevel == old(waitlevel);
- {
- acquire u;
- release u;
- }
-}
-
-class Data {
- var x: int;
- invariant acc(x) && 0 <= x && x < 100;
- method Init()
- requires acc(x);
- ensures acc(x) && x == 0;
- {
- x := 0;
- }
-}
-
-class T {
- var d: Data;
- invariant rd(d) && d != null && rd(d.mu) && rd(this.mu) && this << d;
- method run()
- requires rd(mu) && waitlevel << this;
- ensures rd(mu);
- {
- acquire this;
- acquire d;
- d.x := d.x + 1;
- if (d.x == 100) { d.x := 0; }
- release d;
- release this;
- }
-}
-
-class U {
- method run()
- requires rd(mu) && waitlevel << this;
- ensures rd(mu);
- {
- }
-}
-
-// Tests that use OLD in postcondition of run:
-
-class X {
- var k: int
- var l: int
-
- method inc()
- requires acc(k)
- ensures acc(k) && k == old(k) + 1
- {
- k := k + 1
- }
- method Client0() returns (y: int)
- ensures y == 8
- {
- var x := new X
- x.k := 17 x.l := 10
- call x.inc()
- assert x.k == 18 && x.l == 10
- y := x.k - x.l
- }
-
- method run()
- requires acc(k) && 0 <= k
- ensures acc(k) && k == old(k) + 1
- {
- k := k + 1
- }
-
- method Client1() returns (y: int)
- ensures y == 8
- {
- var x := new X
- x.k := 17
- x.l := 20
- var xToken: token<X.run>;
- fork xToken := x.run();
- x.l := 10
- join xToken
- assert x.k == 18 && x.l == 10
- y := x.k - x.l
- }
- method Client2(tk: token<X.run>, x: X) returns (z: int)
- requires x!=null && tk!=null && acc(tk.joinable) && tk.joinable && eval(tk.fork x.run(), acc(x.k) && 0<=x.k);
- ensures 1 <= z
- {
- join tk
- z := x.k
- assert 1<=x.k;
- }
-}
-
-class ReadSharing {
- var x: int
-
- method Consume()
- requires rd(x,1)
- {
- // skip
- }
-
- method Divulge() // bad
- requires rd(x,1)
- {
- call Consume()
- call Consume() // error: cannot share twice (1773)
- }
-
- method Communicates() // good
- requires rd(x,3)
- ensures rd(x,1)
- {
- call Consume()
- call Consume()
- }
-
- method Gossips() // bad
- requires rd(x,3)
- ensures rd(x,1)
- {
- call Consume()
- call Consume()
- call Consume()
- } // error: does not live up to postcondition (2015)
-
- method Shares() // good
- requires rd*(x)
- ensures rd*(x)
- {
- call Consume()
- call Consume()
- call Consume()
- }
-
- method TeamPlayer(N: int) // good
- requires 0<N && rd(x,N)
- {
- var n := N
- while (1 < n)
- invariant 0<n && rd(x,n)
- {
- n := n - 1
- }
- }
-
- method Unselfish(N: int) // good
- requires rd*(x)
- ensures rd*(x)
- {
- var n := N
- if (N == 173) {
- call Unselfish(200)
- }
- while (0 < n)
- invariant rd*(x)
- {
- call Consume()
- n := n - 1
- }
- }
-}
diff --git a/Chalice/tests/examples/prog3.output.txt b/Chalice/tests/examples/prog3.output.txt deleted file mode 100644 index 18d05658..00000000 --- a/Chalice/tests/examples/prog3.output.txt +++ /dev/null @@ -1,11 +0,0 @@ -Verification of prog3.chalice using parameters=""
-
- 76.3: The postcondition at 77.13 might not hold. The expression at 77.13 might not evaluate to true. - 76.3: Method might lock/unlock more than allowed. - 191.5: The precondition at 182.14 might not hold. Insufficient epsilons at 182.14 for ReadSharing.x. - 202.3: The postcondition at 204.13 might not hold. Insufficient epsilons at 204.13 for ReadSharing.x. - -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.
diff --git a/Chalice/tests/examples/prog4.chalice b/Chalice/tests/examples/prog4.chalice deleted file mode 100644 index 3c655c71..00000000 --- a/Chalice/tests/examples/prog4.chalice +++ /dev/null @@ -1,53 +0,0 @@ -class LoopTargets {
- method M() returns (y) {
- y := 0
- while (y < 100) { y := y + 1 }
- assert y == 0 // error (139)
- }
- method N() returns (t: LoopTargets)
- lockchange t
- {
- t := new LoopTargets
- share t
- acquire t
- var s := true
- while (s)
- lockchange t
- {
- release t // error: loop invariant does not say holds(t) (252)
- s := false
- }
- }
- method P() {
- var t := new LoopTargets
- share t
- acquire t
- var s := true
- while (s)
- invariant acc(t.mu) && waitlevel == t.mu
- lockchange t
- {
- release t // error: loop invariant does not say holds(t) (414)
- acquire t
- s := false
- }
- release t
- }
- method Q() {
- var t := new LoopTargets
- share t
- acquire t
- var s := true
- while (s)
- invariant rd(t.mu)
- invariant holds(t) && waitlevel == t.mu
- lockchange t
- {
- release t
- acquire t
- s := false
- }
- assert holds(t) // there we are
- release t
- }
-}
diff --git a/Chalice/tests/examples/prog4.output.txt b/Chalice/tests/examples/prog4.output.txt deleted file mode 100644 index 9415df7c..00000000 --- a/Chalice/tests/examples/prog4.output.txt +++ /dev/null @@ -1,14 +0,0 @@ -Verification of prog4.chalice using parameters=""
-
- 5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true. - 17.7: The target of the release statement might not be locked by the current thread. - 17.7: Release might fail because the current thread might hold the read lock. - 30.7: The target of the release statement might not be locked by the current thread. - 30.7: Release might fail because the current thread might hold the read lock. - 34.5: The target of the release statement might not be locked by the current thread. - 34.5: Release might fail because the current thread might hold the read lock. - -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.
diff --git a/Chalice/tests/examples/quantifiers.chalice b/Chalice/tests/examples/quantifiers.chalice deleted file mode 100644 index 7377ca3f..00000000 --- a/Chalice/tests/examples/quantifiers.chalice +++ /dev/null @@ -1,59 +0,0 @@ -class A { - var f: int; -} - -class Quantifiers { - var bamboo: seq<A>; - - method test1(a: seq<int>, b: int) - requires b in a; - requires b > 0; - { - assert exists j in a :: true && j > 0; - assert exists j:int :: 0 <= j && j < |a| && a[j] > 0; - assert forall j in a :: exists k in a :: k > 0; - } - - method test2(a: seq<A>) - requires rd(a[*].*); - requires |a| > 0; - requires forall i in a :: i != null && i.f > 0; - { - assert a[0].f > 0; - assert forall j: A :: j in a && j != null ==> j.f > 0; - assert exists j: A :: j in a && j != null && j.f > 0; - } - - method test3(a: seq<A>) - requires |a| > 0; - requires acc(a[*].f); - { - var c := new A; - assert c != a[0]; - } -} - -class Functions { - var x: int; - var y: int; - - function test1(): int - requires acc(this.*); - { - x + y - } - - function test2(): int - requires acc(x) && acc(y); - { - x + y - } - - function test3(a: seq<A>): int - requires acc(a[*].f); - requires forall x in a :: x != null; - requires forall i,j in [0..|a|] :: i != j ==> a[i] != a[j]; - { - |a| == 0 ? 0 : a[0].f + test3(a[1..]) - } -} diff --git a/Chalice/tests/examples/quantifiers.output.txt b/Chalice/tests/examples/quantifiers.output.txt deleted file mode 100644 index 2f325c42..00000000 --- a/Chalice/tests/examples/quantifiers.output.txt +++ /dev/null @@ -1,5 +0,0 @@ -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.
|