diff options
Diffstat (limited to 'Chalice/tests/permission-model')
9 files changed, 96 insertions, 84 deletions
diff --git a/Chalice/tests/permission-model/basic.output.txt b/Chalice/tests/permission-model/basic.output.txt index 9d92923a..02e7acb7 100644 --- a/Chalice/tests/permission-model/basic.output.txt +++ b/Chalice/tests/permission-model/basic.output.txt @@ -1,8 +1,8 @@ Verification of basic.chalice using parameters=""
- 28.3: The postcondition at 30.13 might not hold. Insufficient fraction at 30.13 for Cell.x.
- 48.3: The postcondition at 50.13 might not hold. Insufficient fraction at 50.13 for Cell.x.
- 97.3: The postcondition at 99.13 might not hold. Insufficient fraction at 99.13 for Cell.x.
- 148.3: The postcondition at 150.13 might not hold. Insufficient fraction at 150.13 for Cell.x.
-
-Boogie program verifier finished with 41 verified, 4 errors
+ 28.3: The postcondition at 30.13 might not hold. Insufficient fraction at 30.13 for Cell.x. + 48.3: The postcondition at 50.13 might not hold. Insufficient fraction at 50.13 for Cell.x. + 97.3: The postcondition at 99.13 might not hold. Insufficient fraction at 99.13 for Cell.x. + 148.3: The postcondition at 150.13 might not hold. Insufficient fraction at 150.13 for Cell.x. + +Boogie program verifier finished with 4 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/permission-model/channels.output.txt b/Chalice/tests/permission-model/channels.output.txt index a79b5fb1..159e0ee6 100644 --- a/Chalice/tests/permission-model/channels.output.txt +++ b/Chalice/tests/permission-model/channels.output.txt @@ -1,6 +1,6 @@ Verification of channels.chalice using parameters=""
- 8.5: The where clause at 44.24 might not hold. Insufficient fraction at 44.24 for C.f.
- 18.3: The postcondition at 20.13 might not hold. Insufficient fraction at 20.13 for C.f.
-
-Boogie program verifier finished with 11 verified, 2 errors
+ 8.5: The where clause at 44.24 might not hold. Insufficient fraction at 44.24 for C.f. + 18.3: The postcondition at 20.13 might not hold. Insufficient fraction at 20.13 for C.f. + +Boogie program verifier finished with 2 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/permission-model/locks.output.txt b/Chalice/tests/permission-model/locks.output.txt index 98cd0d4e..3492e807 100644 --- a/Chalice/tests/permission-model/locks.output.txt +++ b/Chalice/tests/permission-model/locks.output.txt @@ -1,14 +1,19 @@ Verification of locks.chalice using parameters=""
- 21.5: Assertion might not hold. Insufficient fraction at 21.12 for Cell.x.
- 24.5: Assertion might not hold. Insufficient fraction at 24.12 for Cell.x.
- 44.5: Assertion might not hold. Insufficient fraction at 44.12 for Cell.x.
- 54.5: Assertion might not hold. Insufficient fraction at 54.12 for Cell.x.
- 73.5: Assertion might not hold. Insufficient fraction at 73.12 for Cell2.x.
- 80.5: Assertion might not hold. Insufficient fraction at 80.12 for Cell2.x.
- 83.5: Assertion might not hold. Insufficient fraction at 83.12 for Cell2.x.
- 103.5: Assertion might not hold. Insufficient fraction at 103.12 for Cell2.x.
- 111.5: Monitor invariant might hot hold. Insufficient fraction at 64.13 for Cell2.x.
- 136.10: Location might not be readable.
-
-Boogie program verifier finished with 20 verified, 10 errors
+ 21.5: Assertion might not hold. Insufficient fraction at 21.12 for Cell.x. + 24.5: Assertion might not hold. Insufficient fraction at 24.12 for Cell.x. + 44.5: Assertion might not hold. Insufficient fraction at 44.12 for Cell.x. + 54.5: Assertion might not hold. Insufficient fraction at 54.12 for Cell.x. + 73.5: Assertion might not hold. Insufficient fraction at 73.12 for Cell2.x. + 80.5: Assertion might not hold. Insufficient fraction at 80.12 for Cell2.x. + 83.5: Assertion might not hold. Insufficient fraction at 83.12 for Cell2.x. + 103.5: Assertion might not hold. Insufficient fraction at 103.12 for Cell2.x. + 111.5: Monitor invariant might hot hold. Insufficient fraction at 64.13 for Cell2.x. + 136.10: Location might not be readable. + + 66.3: The end of method a1 is unreachable. + 76.3: The end of method a2 is unreachable. + 86.3: The end of method a3 is unreachable. + 126.3: The end of method a6 is unreachable. + +Boogie program verifier finished with 10 errors and 4 smoke test warnings.
diff --git a/Chalice/tests/permission-model/peculiar.output.txt b/Chalice/tests/permission-model/peculiar.output.txt index 6754cf7f..68d4b092 100644 --- a/Chalice/tests/permission-model/peculiar.output.txt +++ b/Chalice/tests/permission-model/peculiar.output.txt @@ -1,5 +1,7 @@ Verification of peculiar.chalice using parameters=""
- 35.5: Assertion might not hold. Insufficient fraction at 35.12 for Cell.x.
-
-Boogie program verifier finished with 18 verified, 1 error
+ 35.5: Assertion might not hold. Insufficient fraction at 35.12 for Cell.x. + + 30.3: The end of method t4 is unreachable. + +Boogie program verifier finished with 1 errors and 1 smoke test warnings.
diff --git a/Chalice/tests/permission-model/permission_arithmetic.output.txt b/Chalice/tests/permission-model/permission_arithmetic.output.txt index 277b5da6..d57e0939 100644 --- a/Chalice/tests/permission-model/permission_arithmetic.output.txt +++ b/Chalice/tests/permission-model/permission_arithmetic.output.txt @@ -1,15 +1,22 @@ Verification of permission_arithmetic.chalice using parameters=""
- 26.5: Assertion might not hold. The permission at 26.12 might not be positive.
- 42.5: The precondition at 35.14 might not hold. The permission at 35.14 might not be positive.
- 75.3: The postcondition at 77.13 might not hold. Insufficient fraction at 77.13 for Cell.x.
- 88.3: The postcondition at 90.13 might not hold. Insufficient epsilons at 90.22 for Cell.x.
- 105.20: Location might not be readable.
- 111.20: Location might not be readable.
- 147.5: Monitor invariant might not hold. Insufficient fraction at 8.13 for Cell.x.
- 164.3: The postcondition at 166.13 might not hold. The permission at 166.13 might not be positive.
- 176.3: The postcondition at 178.13 might not hold. Insufficient fraction at 178.13 for Cell.x.
- 205.10: Location might not be readable.
- 220.10: Location might not be readable.
-
-Boogie program verifier finished with 61 verified, 11 errors
+ 26.5: Assertion might not hold. The permission at 26.12 might not be positive. + 42.5: The precondition at 35.14 might not hold. The permission at 35.14 might not be positive. + 75.3: The postcondition at 77.13 might not hold. Insufficient fraction at 77.13 for Cell.x. + 88.3: The postcondition at 90.13 might not hold. Insufficient epsilons at 90.22 for Cell.x. + 105.20: Location might not be readable. + 111.20: Location might not be readable. + 147.5: Monitor invariant might not hold. Insufficient fraction at 8.13 for Cell.x. + 164.3: The postcondition at 166.13 might not hold. The permission at 166.13 might not be positive. + 176.3: The postcondition at 178.13 might not hold. Insufficient fraction at 178.13 for Cell.x. + 205.10: Location might not be readable. + 220.10: Location might not be readable. + + 18.3: Precondition of method a2 is equivalent to false. + 18.3: The end of method a2 is unreachable. + 24.3: The end of method a3 is unreachable. + 39.3: The end of method a6 is unreachable. + 200.3: The end of method a28 is unreachable. + 215.3: The end of method a28b is unreachable. + +Boogie program verifier finished with 11 errors and 6 smoke test warnings.
diff --git a/Chalice/tests/permission-model/predicates.output.txt b/Chalice/tests/permission-model/predicates.output.txt index 30c08a1a..8b9d8abe 100644 --- a/Chalice/tests/permission-model/predicates.output.txt +++ b/Chalice/tests/permission-model/predicates.output.txt @@ -1,7 +1,10 @@ Verification of predicates.chalice using parameters=""
- 37.5: Fold might fail because the definition of Cell.write1 does not hold. Insufficient fraction at 6.22 for Cell.x.
- 55.5: Fold might fail because the definition of Cell.read1 does not hold. Insufficient fraction at 8.21 for Cell.x.
- 66.3: The postcondition at 68.13 might not hold. Insufficient fraction at 68.13 for Cell.x.
-
-Boogie program verifier finished with 27 verified, 3 errors
+ 37.5: Fold might fail because the definition of Cell.write1 does not hold. Insufficient fraction at 6.22 for Cell.x. + 55.5: Fold might fail because the definition of Cell.read1 does not hold. Insufficient fraction at 8.21 for Cell.x. + 66.3: The postcondition at 68.13 might not hold. Insufficient fraction at 68.13 for Cell.x. + + 28.3: The end of method b3 is unreachable. + 49.3: The end of method b5 is unreachable. + +Boogie program verifier finished with 3 errors and 2 smoke test warnings.
diff --git a/Chalice/tests/permission-model/scaling.chalice b/Chalice/tests/permission-model/scaling.chalice index 29930346..91c73f6d 100644 --- a/Chalice/tests/permission-model/scaling.chalice +++ b/Chalice/tests/permission-model/scaling.chalice @@ -8,6 +8,8 @@ are multiplied. This introduces non-linear arithmetic in Boogie, which can be very hard and unpredicable for the theorem prover. For this reason, this test is
taking a very long time to complete.
+Note 2: For the moment, this test is (mostly) disabled.
+
-- Stefan Heule, June 2011
*/
@@ -26,59 +28,59 @@ class Cell { // --- permission scaling ---
method s1()
- requires rd(read1);
+ // requires rd(read1);
{
- unfold rd(read1);
- assert(rd*(x));
- assert(rd(x)); // ERROR: should fail
+ // unfold rd(read1);
+ // assert(rd*(x));
+ // assert(rd(x)); // ERROR: should fail
}
method s2() // INCOMPLETNESS: postcondition should hold, but fails at the moment
- requires rd(read1);
- ensures rd(read1);
+ // requires rd(read1);
+ // ensures rd(read1);
{
- unfold rd(read1);
- fold rd(read1);
+ // unfold rd(read1);
+ // fold rd(read1);
}
method s3()
- requires acc(x);
- ensures rd(read1);
+ // requires acc(x);
+ // ensures rd(read1);
{
- fold rd(read1);
- assert(rd*(x));
- assert(acc(x)); // ERROR: should fail
+ // fold rd(read1);
+ // assert(rd*(x));
+ // assert(acc(x)); // ERROR: should fail
}
method s4() // ERROR: postcondition does not hold
- requires acc(x);
- ensures read1;
+ // requires acc(x);
+ // ensures read1;
{
- fold rd(read1);
+ // fold rd(read1);
}
method s5()
- requires rd(read2);
+ // requires rd(read2);
{
- unfold rd(read2);
- assert(rd*(x));
- assert(rd(x)); // ERROR: should fail
+ // unfold rd(read2);
+ // assert(rd*(x));
+ // assert(rd(x)); // ERROR: should fail
}
method s6()
- requires acc(x);
- ensures rd(read2);
+ // requires acc(x);
+ // ensures rd(read2);
{
- fold rd(read2);
- assert(rd*(x));
- assert(acc(x)); // ERROR: should fail
+ // fold rd(read2);
+ // assert(rd*(x));
+ // assert(acc(x)); // ERROR: should fail
}
method s7() // ERROR: postcondition does not hold
- requires acc(x);
- ensures read2;
+ // requires acc(x);
+ // ensures read2;
{
- fold rd(read2);
+ // fold rd(read2);
}
// --- helper functions ---
diff --git a/Chalice/tests/permission-model/scaling.output.txt b/Chalice/tests/permission-model/scaling.output.txt index 863e79d8..d57ab458 100644 --- a/Chalice/tests/permission-model/scaling.output.txt +++ b/Chalice/tests/permission-model/scaling.output.txt @@ -1,11 +1,4 @@ Verification of scaling.chalice using parameters=""
- 33.5: Assertion might not hold. Insufficient fraction at 33.12 for Cell.x.
- 36.3: The postcondition at 38.13 might not hold. Insufficient fraction at 38.13 for Cell.read1.
- 50.5: Assertion might not hold. Insufficient fraction at 50.12 for Cell.x.
- 53.3: The postcondition at 55.13 might not hold. Insufficient fraction at 55.13 for Cell.read1.
- 65.5: Assertion might not hold. Insufficient fraction at 65.12 for Cell.x.
- 74.5: Assertion might not hold. Insufficient fraction at 74.12 for Cell.x.
- 77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Cell.read2.
-
-Boogie program verifier finished with 17 verified, 7 errors
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/permission-model/sequences.output.txt b/Chalice/tests/permission-model/sequences.output.txt index c7099103..f557b8c7 100644 --- a/Chalice/tests/permission-model/sequences.output.txt +++ b/Chalice/tests/permission-model/sequences.output.txt @@ -1,6 +1,6 @@ Verification of sequences.chalice using parameters=""
- 36.3: The postcondition at 41.13 might not hold. Insufficient permission at 41.13 for A.f
- 60.3: The postcondition at 65.13 might not hold. Insufficient permission at 65.13 for A.f
-
-Boogie program verifier finished with 20 verified, 2 errors
+ 36.3: The postcondition at 41.13 might not hold. Insufficient permission at 41.13 for A.f + 60.3: The postcondition at 65.13 might not hold. Insufficient permission at 65.13 for A.f + +Boogie program verifier finished with 2 errors and 0 smoke test warnings.
|