diff options
| author |  stefanheule <unknown> | 2011-07-21 18:37:32 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-07-21 18:37:32 +0200 |
| commit | 551a036367503c85a42c1452f3f72475cc218f3d (patch) | |
| tree | 7add8584e758a62119c1f3b1d6b607e10459d642 | |
| parent | f728aa881caee16eaf6b5d25262578d64059f7f2 (diff) | |
Chalice: Only show the "first" smoke warning, as once the prover is able to show false, all follwoing attempts will always succeed. However, smoke warnings on different paths through a method are still all reported.
Also, the places where to insert "assert false" are chosen more carefully (essentially always all statements that inhale something).
Update test reference outputs accordingly.
28 files changed, 215 insertions, 91 deletions
diff --git a/Chalice/src/SmokeTest.scala b/Chalice/src/SmokeTest.scala index 9e141e31..bf2622ce 100644 --- a/Chalice/src/SmokeTest.scala +++ b/Chalice/src/SmokeTest.scala @@ -13,8 +13,24 @@ import scala.util.parsing.input.NoPosition */
object SmokeTest {
- /** Map from error message ID's to their position and error message */
- private var errorMessages: scala.collection.SortedMap[Int, (Position, String)] = scala.collection.SortedMap()
+ /** SmokeAssert is used to keep track of the position and real error message
+ * associated with a certain assert statement. Also, we build a DAG of
+ * SmokeAssert that essentially corresponds to the control flow graph (the
+ * member prev is used to record the in-edges of every SmokeAssert). This
+ * graph is then used to omit certain warnings (e.g., if the precondition is
+ * already false, we do not need to report that the method end cannot be
+ * reached, too).
+ */
+ case class SmokeAssert(id: Int, pos: Position, msg: String, prev: Set[SmokeAssert], chaliceAssert: Assert) {
+ var warning: Boolean = false // did this "assert false" generate a warning? (i.e. did it not generate a Boogie error?)
+ }
+ /** Serves as a sentinel for the first assert (which should always cause a
+ * warning, thus SmokeAssertSentinel.warning = false
+ */
+ object SmokeAssertSentinel extends SmokeAssert(-1, NoPosition, "", Set(), null)
+
+ /** Map from error message ID's to their SmokeAssert object */
+ private var smokeAssertions: Map[Int,SmokeAssert] = Map()
private var count: Int = 0 // current error message id
/** Process the output of Boogie and generate the correct warnings from smoke testing */
@@ -30,26 +46,38 @@ object SmokeTest { case SummaryPattern(verified, errors) => outcome = Some((verified.toInt,errors.toInt))
case _ => verificationResult += s + "\n"
}
- val smokeTestAssertions = errorMessages.size
- val smokeTestWarnings = smokeTestAssertions - smokeErrors.size
+ // check which smoke assertions failed
+ for ((errNr, s@SmokeAssert(_, pos, msg, prev, _)) <- smokeAssertions) yield {
+ s.warning = !smokeErrors.contains(errNr)
+ }
+
+ var smokeTestWarnings = 0
val smokeResult = {
var t = "";
- for ((errNr, (pos, msg)) <- errorMessages) yield {
- if (!smokeErrors.contains(errNr)) {
- t += " " + pos + ": " + msg + "\n"
+ for (s@SmokeAssert(_, pos, msg, prev, _) <- smokeAssertions.values.toList.sortWith((a,b) => a.pos < b.pos)) yield {
+ if (s.warning) {
+ if (s.prev.exists(a => !a.warning)) { // omit warning if all ancestors created a warning
+ t += " " + pos + ": " + msg + "\n"
+ smokeTestWarnings += 1
+ }
}
}
t
}
- verificationResult +
- smokeResult + (if (smokeResult != "") "\n" else "") +
- (outcome match {
+ var realErrors = -1
+ val status = (outcome match {
case None => ""
case Some((verified,errors)) =>
- "Boogie program verifier finished with " + (errors-smokeErrors.size) + " errors and " + smokeTestWarnings + " smoke test warnings."
+ realErrors = errors-smokeErrors.size
+ "Boogie program verifier finished with " + realErrors + " errors and " + smokeTestWarnings + " smoke test warnings."
})
+
+ verificationResult +
+ (if (realErrors > 0) "The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.\n" else "") +
+ smokeResult + (if (smokeResult != "") "\n" else "") +
+ status
}
/** Add smoke assertions for to a program. */
@@ -74,61 +102,108 @@ object SmokeTest { /** Add smoke assertions for a method (if necessary). */
private def smokeMethod(method: Method) = {
- var newbody = smokeStmt(method.body)
- val preassert = smokeAssert(method.pos, "Precondition of method " + method.Id + " is equivalent to false.")
- val postassert = smokeAssert(method.pos, "The end of method " + method.Id + " is unreachable.")
- newbody = preassert :: newbody ::: postassert :: Nil
+ val preassert = initSmokeAssert(method.pos, "Precondition of method " + method.Id + " is equivalent to false.")
+ var (newbody, bodyout) = smokeStmt(method.body, Set(preassert))
+ val postassert = initSmokeAssert(method.pos, "The end of method " + method.Id + " is unreachable.", bodyout)
+ newbody = preassert.chaliceAssert :: newbody ::: postassert.chaliceAssert :: Nil
Method(method.id, method.ins, method.outs, method.spec, newbody)
}
/** Add smoke assertions for multiple statements (if necessary). */
- private def smokeStmt(stmts: List[Statement]): List[Statement] = {
- (for (s <- stmts) yield copyPosition(s, smokeStmt(s))).flatten
+ private def smokeStmt(stmts: List[Statement], in: Set[SmokeAssert]): (List[Statement], Set[SmokeAssert]) = {
+ var tmp = in
+ val newstmts = (for (s <- stmts) yield {
+ val (sstmts, sout) = smokeStmt(s, tmp)
+ tmp = sout
+ copyPosition(s, sstmts)
+ }).flatten
+ (newstmts, tmp)
}
/** Add smoke assertions for a statement (if necessary). */
- private def smokeStmt(stmt: Statement): List[Statement] = {
- stmt match {
- case Assume(_) => stmt :: smokeAssert(stmt.pos, "Assumption might introduce a contradiction.") :: Nil
- case BlockStmt(ss) => smokeStmt(ss)
+ private def smokeStmt(stmt: Statement, in: Set[SmokeAssert]): (List[Statement], Set[SmokeAssert]) = {
+ var out = in
+ val result = stmt match {
+ // composite statements
+ case BlockStmt(ss) =>
+ val (smokestmts, blocksmoke) = smokeStmt(ss, in)
+ out = blocksmoke
+ smokestmts
case ifs@IfStmt(guard, BlockStmt(then), els) =>
- val newthen = smokeStmt(then) ::: smokeAssert(ifs.pos, "The end of the if-branch is unreachable.") :: Nil
+ val thensmoke = initSmokeAssert(ifs.pos, "The begging of the if-branch is unreachable.", in)
+ val (thensmokestmts, thenout) = smokeStmt(then, Set(thensmoke))
+ out = thenout
+ val newthen = thensmoke.chaliceAssert :: thensmokestmts
val newelse = els match {
- case None => None
- case Some(s) => Some(BlockStmt(smokeStmt(s) ::: smokeAssert(ifs.pos, "The end of the else-branch is unreachable.") :: Nil))
+ case None =>
+ out ++= in
+ None
+ case Some(s) =>
+ val elsesmoke = initSmokeAssert(ifs.pos, "The begging of the else-branch is unreachable.", in)
+ val (blocksmokestmts, blockout) = smokeStmt(s, Set(elsesmoke))
+ out ++= blockout
+ Some(BlockStmt(elsesmoke.chaliceAssert :: blocksmokestmts))
}
IfStmt(guard, BlockStmt(newthen), newelse) :: Nil
case WhileStmt(guard, oldInvs, newInvs, lkch, BlockStmt(body)) =>
- val newbody = smokeStmt(body) ::: smokeAssert(stmt.pos, "The end of the while-body is unreachable.") :: Nil
- WhileStmt(guard, oldInvs, newInvs, lkch, BlockStmt(newbody)) :: Nil
+ val whilesmoke = initSmokeAssert(stmt.pos, "The begging of the while-body is unreachable.", in)
+ val (whilesmokestmts, whileout) = smokeStmt(body, Set(whilesmoke))
+ val whileaftersmoke = initSmokeAssert(stmt.pos, "The statements after the while-loop are unreachable.", in)
+ val whileendsmoke = initSmokeAssert(stmt.pos, "The end of the while-loop is unreachable.", whileout)
+ out = Set(whileaftersmoke)
+ val newbody = whilesmoke.chaliceAssert :: whilesmokestmts ::: whileendsmoke.chaliceAssert :: Nil
+ WhileStmt(guard, oldInvs, newInvs, lkch, BlockStmt(newbody)) :: whileaftersmoke.chaliceAssert :: Nil
case Lock(obj, BlockStmt(body), rdLock) =>
- Lock(obj, BlockStmt(smokeStmt(body)), rdLock) :: Nil
- case _: RefinementBlock => stmt :: Nil
+ val locksmoke = initSmokeAssert(stmt.pos, "The begging of the lock-block is unreachable.", in)
+ val (blocksmokestmts, blockout) = smokeStmt(body, Set(locksmoke))
+ out = blockout
+ Lock(obj, BlockStmt(locksmoke.chaliceAssert :: blocksmokestmts), rdLock) :: Nil
+ case _: RefinementBlock =>
+ // TODO
+ stmt :: Nil
+
+ // assumption
+ case Assume(_) =>
+ val assumeSmoke = initSmokeAssert(stmt.pos, "Assumption introduces a contradiction.", in)
+ out = Set(assumeSmoke)
+ stmt :: assumeSmoke.chaliceAssert :: Nil
+ // simple statements that inhale something
+ case Unfold(_) => val (stmts, sout) = smokeSimpleStmt(stmt, in, "unfold"); out = sout; stmts
+ case JoinAsync(_, _) => val (stmts, sout) = smokeSimpleStmt(stmt, in, "join"); out = sout; stmts
+ case _: Call => val (stmts, sout) = smokeSimpleStmt(stmt, in, "method call"); out = sout; stmts
+ case _: SpecStmt => val (stmts, sout) = smokeSimpleStmt(stmt, in, "specification"); out = sout; stmts
+ case Receive(_, _, _) => val (stmts, sout) = smokeSimpleStmt(stmt, in, "receive"); out = sout; stmts
+ case Acquire(_) => val (stmts, sout) = smokeSimpleStmt(stmt, in, "acquire"); out = sout; stmts
+ case RdAcquire(_) => val (stmts, sout) = smokeSimpleStmt(stmt, in, "rd acquire"); out = sout; stmts
+
+ // any other simple statements
case Assert(_) => stmt :: Nil
case Assign(_, _) => stmt :: Nil
case FieldUpdate(_, _) => stmt :: Nil
case _: LocalVar => stmt :: Nil
- case _: SpecStmt => stmt :: Nil
- case _: Call => stmt :: Nil
case Install(_, _, _) => stmt :: Nil
case Share(_, _, _) => stmt :: Nil
case Unshare(_) => stmt :: Nil
- case Acquire(_) => stmt :: Nil
case Release(_) => stmt :: Nil
- case RdAcquire(_) => stmt :: Nil
case RdRelease(_) => stmt :: Nil
case Downgrade(_) => stmt :: Nil
case Free(_) => stmt :: Nil
case Fold(_) => stmt :: Nil
- case Unfold(_) => stmt :: Nil
case CallAsync(_, _, _, _, _) => stmt :: Nil
- case JoinAsync(_, _) => stmt :: Nil
case Send(_, _) => stmt :: Nil
- case Receive(_, _, _) => stmt :: Nil
case _: Signal => stmt :: Nil
case _: Wait => stmt :: Nil
}
+ (result, out)
+ }
+
+ /** Helper method to add a smoke assertion after a simple (non-compound)
+ * statement.
+ */
+ def smokeSimpleStmt(stmt: Statement, in: Set[SmokeAssert], msg: String): (List[Statement], Set[SmokeAssert]) = {
+ val smoke = initSmokeAssert(stmt.pos, "The statements after the " + msg + " statement are unreachable.", in)
+ (stmt :: smoke.chaliceAssert :: Nil, Set(smoke))
}
/** Generate an "assert false" with a certain position and a certain error
@@ -137,13 +212,17 @@ object SmokeTest { * not generate warnings for all failing assertions (even if the command
* line switch /subsumption:0 is used).
*/
- private def smokeAssert(pos: Position, error: String) = {
+ def initSmokeAssert(pos: Position, error: String): SmokeAssert = initSmokeAssert(pos, error, Set(SmokeAssertSentinel))
+ def initSmokeAssert(pos: Position, error: String, prev: Set[SmokeAssert]): SmokeAssert = {
count += 1
- errorMessages += count -> (pos, error)
- val assert = Assert(Neq(IntLiteral(1), IntLiteral(1)))
+ val i = IntLiteral(1); i.typ = IntClass
+ val n = Neq(i, i); n.typ = BoolClass
+ val assert = Assert(n)
assert.smokeErrorNr = Some(count)
assert.pos = pos
- assert
+ val sm = SmokeAssert(count, pos, error, prev, assert)
+ smokeAssertions += count -> sm
+ sm
}
/** Copy the position of an old AST node to a new node (if not already
diff --git a/Chalice/tests/examples/AssociationList.output.txt b/Chalice/tests/examples/AssociationList.output.txt index ce20ed93..bfff3c60 100644 --- a/Chalice/tests/examples/AssociationList.output.txt +++ b/Chalice/tests/examples/AssociationList.output.txt @@ -3,11 +3,8 @@ Verification of AssociationList.chalice using parameters="" 19.3: The postcondition at 21.13 might not hold. Insufficient fraction at 21.13 for mu. 64.9: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop. - 75.11: The end of the if-branch is unreachable. - 79.13: The end of the if-branch is unreachable. - 79.13: The end of the else-branch is unreachable. - 75.11: The end of the else-branch is unreachable. - 64.9: The end of the while-body is unreachable. - 60.7: The end of the else-branch is unreachable. +The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. + 64.9: The begging of the while-body is unreachable. + 64.9: The statements after the while-loop are unreachable. -Boogie program verifier finished with 2 errors and 6 smoke test warnings.
+Boogie program verifier finished with 2 errors and 2 smoke test warnings.
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt index 6ea31348..b47290ea 100644 --- a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt @@ -1,11 +1,8 @@ Verification of CopyLessMessagePassing-with-ack.chalice using parameters=""
- 48.22: Assumption might introduce a contradiction. - 48.7: The end of the if-branch is unreachable. - 69.22: Assumption might introduce a contradiction. - 69.7: The end of the if-branch is unreachable. - 72.21: Assumption might introduce a contradiction. - 72.5: The end of the if-branch is unreachable. + 48.22: Assumption introduces a contradiction. + 69.22: Assumption introduces a contradiction. + 72.21: Assumption introduces a contradiction. -Boogie program verifier finished with 0 errors and 6 smoke test warnings.
+Boogie program verifier finished with 0 errors and 3 smoke test warnings.
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt index 7f53cfb3..42a63bf1 100644 --- a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt @@ -1,9 +1,7 @@ Verification of CopyLessMessagePassing-with-ack2.chalice using parameters=""
- 50.23: Assumption might introduce a contradiction. - 50.7: The end of the if-branch is unreachable. - 65.27: Assumption might introduce a contradiction. - 65.7: The end of the if-branch is unreachable. + 50.23: Assumption introduces a contradiction. + 65.27: Assumption introduces a contradiction. -Boogie program verifier finished with 0 errors and 4 smoke test warnings.
+Boogie program verifier finished with 0 errors and 2 smoke test warnings.
diff --git a/Chalice/tests/examples/LoopLockChange.output.txt b/Chalice/tests/examples/LoopLockChange.output.txt index 50b446ec..19e84f93 100644 --- a/Chalice/tests/examples/LoopLockChange.output.txt +++ b/Chalice/tests/examples/LoopLockChange.output.txt @@ -4,9 +4,9 @@ Verification of LoopLockChange.chalice using parameters="" 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. - 10.5: The end of the while-body is unreachable. - 3.3: The end of method Test0 is unreachable. - 75.5: Assumption might introduce a contradiction. - 59.3: The end of method Test4 is unreachable. +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 4 smoke test warnings.
+Boogie program verifier finished with 3 errors and 3 smoke test warnings.
diff --git a/Chalice/tests/examples/PetersonsAlgorithm.output.txt b/Chalice/tests/examples/PetersonsAlgorithm.output.txt index 185dc8e1..eddb4927 100644 --- a/Chalice/tests/examples/PetersonsAlgorithm.output.txt +++ b/Chalice/tests/examples/PetersonsAlgorithm.output.txt @@ -1,8 +1,8 @@ Verification of PetersonsAlgorithm.chalice using parameters=""
- 15.3: The end of method Main is unreachable. - 30.3: The end of method Process0 is unreachable. - 55.3: The end of method Process1 is unreachable. + 23.5: The statements after the while-loop are unreachable. + 34.5: The statements after the while-loop are unreachable. + 59.5: The statements after the while-loop are unreachable. Boogie program verifier finished with 0 errors and 3 smoke test warnings.
diff --git a/Chalice/tests/examples/ProdConsChannel.output.txt b/Chalice/tests/examples/ProdConsChannel.output.txt index fc436ea7..167898fb 100644 --- a/Chalice/tests/examples/ProdConsChannel.output.txt +++ b/Chalice/tests/examples/ProdConsChannel.output.txt @@ -5,6 +5,7 @@ Verification of ProdConsChannel.chalice using parameters="" 85.20: Location might not be readable. 123.7: Assertion might not hold. The expression at 123.14 might not evaluate to true. - 80.5: The end of the while-body is unreachable. +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.
diff --git a/Chalice/tests/examples/SmokeTestTest.chalice b/Chalice/tests/examples/SmokeTestTest.chalice index e5384955..2f32625e 100644 --- a/Chalice/tests/examples/SmokeTestTest.chalice +++ b/Chalice/tests/examples/SmokeTestTest.chalice @@ -1,4 +1,3 @@ -// chalice-parameter=-smoke
// This file is meant as a test for Chalice's smoke testing feature (command line switch -smoke)
class Cell {
var f: int;
@@ -77,4 +76,37 @@ class Cell { 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
+ }
}
diff --git a/Chalice/tests/examples/SmokeTestTest.output.txt b/Chalice/tests/examples/SmokeTestTest.output.txt index 2bfce65f..0d7985d6 100644 --- a/Chalice/tests/examples/SmokeTestTest.output.txt +++ b/Chalice/tests/examples/SmokeTestTest.output.txt @@ -1,15 +1,19 @@ -Verification of SmokeTestTest.chalice using parameters="-smoke"
+Verification of SmokeTestTest.chalice using parameters=""
+ 103.3: The postcondition at 104.13 might not hold. The expression at 104.13 might not evaluate to true. - 6.3: Precondition of method a1 is equivalent to false. - 6.3: The end of method a1 is unreachable. - 10.3: Precondition of method a2 is equivalent to false. - 10.3: The end of method a2 is unreachable. - 25.5: The end of the if-branch is unreachable. - 41.5: The end of the if-branch is unreachable. - 51.5: Assumption might introduce a contradiction. - 48.3: The end of method a7 is unreachable. - 54.3: The end of method a8 is unreachable. - 74.5: The end of the else-branch is unreachable. +The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. + 5.3: Precondition of method a1 is equivalent to false. + 9.3: Precondition of method a2 is equivalent to false. + 24.5: The begging of the if-branch is unreachable. + 40.5: The begging of the if-branch is unreachable. + 50.5: Assumption introduces a contradiction. + 56.5: The statements after the while-loop are unreachable. + 73.5: The begging of the else-branch is unreachable. + 87.5: The begging of the if-branch is unreachable. + 90.7: The begging of the else-branch is unreachable. + 90.19: Assumption introduces a contradiction. + 97.5: Assumption introduces a contradiction. + 110.5: The statements after the method call statement are unreachable. -Boogie program verifier finished with 0 errors and 10 smoke test warnings.
+Boogie program verifier finished with 1 errors and 12 smoke test warnings.
diff --git a/Chalice/tests/examples/UnboundedThreads.output.txt b/Chalice/tests/examples/UnboundedThreads.output.txt index ccb4e93c..bd34d380 100644 --- a/Chalice/tests/examples/UnboundedThreads.output.txt +++ b/Chalice/tests/examples/UnboundedThreads.output.txt @@ -2,4 +2,5 @@ Verification of UnboundedThreads.chalice using parameters="" 40.17: The loop invariant at 40.17 might not be preserved by the loop. Insufficient epsilons at 40.27 for C.f. +The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. Boogie program verifier finished with 1 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/examples/cell-defaults.output.txt b/Chalice/tests/examples/cell-defaults.output.txt index 31b4223f..138a5717 100644 --- a/Chalice/tests/examples/cell-defaults.output.txt +++ b/Chalice/tests/examples/cell-defaults.output.txt @@ -4,6 +4,7 @@ Verification of cell-defaults.chalice using parameters="-defaults -autoFold -aut 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/cell.output.txt b/Chalice/tests/examples/cell.output.txt index 075cbcf5..b5ba1586 100644 --- a/Chalice/tests/examples/cell.output.txt +++ b/Chalice/tests/examples/cell.output.txt @@ -2,6 +2,7 @@ Verification of cell.chalice using parameters="" 142.5: Assertion might not hold. Insufficient fraction at 142.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. 135.3: The end of method main2 is unreachable. Boogie program verifier finished with 1 errors and 1 smoke test warnings.
diff --git a/Chalice/tests/examples/counter.output.txt b/Chalice/tests/examples/counter.output.txt index 69f93f12..1d5be0ea 100644 --- a/Chalice/tests/examples/counter.output.txt +++ b/Chalice/tests/examples/counter.output.txt @@ -7,10 +7,11 @@ Verification of counter.chalice using parameters="" 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. - 124.3: The end of method nestedBad1 is unreachable. - 132.3: The end of method nestedBad2 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/dining-philosophers.output.txt b/Chalice/tests/examples/dining-philosophers.output.txt index 9d17fd1f..bd1bd4a0 100644 --- a/Chalice/tests/examples/dining-philosophers.output.txt +++ b/Chalice/tests/examples/dining-philosophers.output.txt @@ -1,6 +1,6 @@ Verification of dining-philosophers.chalice using parameters=""
- 16.3: The end of method run is unreachable. + 24.5: The statements after the while-loop are unreachable. Boogie program verifier finished with 0 errors and 1 smoke test warnings.
diff --git a/Chalice/tests/examples/linkedlist.output.txt b/Chalice/tests/examples/linkedlist.output.txt index ce5b5844..468e5921 100644 --- a/Chalice/tests/examples/linkedlist.output.txt +++ b/Chalice/tests/examples/linkedlist.output.txt @@ -2,4 +2,5 @@ Verification of linkedlist.chalice using parameters="" 49.39: Precondition at 47.14 might not hold. The expression at 47.31 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. Boogie program verifier finished with 1 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/examples/producer-consumer.output.txt b/Chalice/tests/examples/producer-consumer.output.txt index 9d408b7d..55f4bf3c 100644 --- a/Chalice/tests/examples/producer-consumer.output.txt +++ b/Chalice/tests/examples/producer-consumer.output.txt @@ -1,7 +1,7 @@ Verification of producer-consumer.chalice using parameters=""
- 36.3: The end of method run is unreachable. - 77.3: The end of method run is unreachable. + 42.5: The statements after the while-loop are unreachable. + 81.5: The statements after the while-loop are unreachable. Boogie program verifier finished with 0 errors and 2 smoke test warnings.
diff --git a/Chalice/tests/examples/prog1.output.txt b/Chalice/tests/examples/prog1.output.txt index 3b80f8a8..630ecdfa 100644 --- a/Chalice/tests/examples/prog1.output.txt +++ b/Chalice/tests/examples/prog1.output.txt @@ -8,6 +8,7 @@ Verification of prog1.chalice using parameters="" 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. diff --git a/Chalice/tests/examples/prog2.output.txt b/Chalice/tests/examples/prog2.output.txt index 3d08e54c..b9d88bbe 100644 --- a/Chalice/tests/examples/prog2.output.txt +++ b/Chalice/tests/examples/prog2.output.txt @@ -5,8 +5,9 @@ Verification of prog2.chalice using parameters="" 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. - 35.3: The end of method Caller2 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.output.txt b/Chalice/tests/examples/prog3.output.txt index 729d78fe..18d05658 100644 --- a/Chalice/tests/examples/prog3.output.txt +++ b/Chalice/tests/examples/prog3.output.txt @@ -5,6 +5,7 @@ Verification of prog3.chalice using parameters="" 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. - 187.3: The end of method Divulge is unreachable. +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.output.txt b/Chalice/tests/examples/prog4.output.txt index db9af8c2..9415df7c 100644 --- a/Chalice/tests/examples/prog4.output.txt +++ b/Chalice/tests/examples/prog4.output.txt @@ -8,6 +8,7 @@ Verification of prog4.chalice using parameters="" 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.output.txt b/Chalice/tests/examples/quantifiers.output.txt index 2f325c42..4abb22e1 100644 --- a/Chalice/tests/examples/quantifiers.output.txt +++ b/Chalice/tests/examples/quantifiers.output.txt @@ -2,4 +2,5 @@ Verification of quantifiers.chalice using parameters="" 57.29: The heap of the callee might not be strictly smaller than the heap of the caller. +The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. Boogie program verifier finished with 1 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/permission-model/basic.output.txt b/Chalice/tests/permission-model/basic.output.txt index 02e7acb7..acbef565 100644 --- a/Chalice/tests/permission-model/basic.output.txt +++ b/Chalice/tests/permission-model/basic.output.txt @@ -5,4 +5,5 @@ Verification of basic.chalice using parameters="" 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. +The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 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 159e0ee6..f588bc0a 100644 --- a/Chalice/tests/permission-model/channels.output.txt +++ b/Chalice/tests/permission-model/channels.output.txt @@ -3,4 +3,5 @@ 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. +The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 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 3492e807..b6ea8f80 100644 --- a/Chalice/tests/permission-model/locks.output.txt +++ b/Chalice/tests/permission-model/locks.output.txt @@ -11,9 +11,10 @@ Verification of locks.chalice using parameters="" 111.5: Monitor invariant might hot hold. Insufficient fraction at 64.13 for Cell2.x. 136.10: 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. 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. + 138.5: The statements after the acquire statement are 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 68d4b092..e2e6ec90 100644 --- a/Chalice/tests/permission-model/peculiar.output.txt +++ b/Chalice/tests/permission-model/peculiar.output.txt @@ -2,6 +2,7 @@ Verification of peculiar.chalice using parameters="" 35.5: Assertion might not hold. Insufficient fraction at 35.12 for Cell.x. +The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 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 d57e0939..f5c02b3d 100644 --- a/Chalice/tests/permission-model/permission_arithmetic.output.txt +++ b/Chalice/tests/permission-model/permission_arithmetic.output.txt @@ -12,11 +12,11 @@ Verification of permission_arithmetic.chalice using parameters="" 205.10: Location might not be readable. 220.10: 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. 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. + 42.5: The statements after the method call statement are 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.
+Boogie program verifier finished with 11 errors and 5 smoke test warnings.
diff --git a/Chalice/tests/permission-model/predicates.output.txt b/Chalice/tests/permission-model/predicates.output.txt index 8b9d8abe..5c0d0455 100644 --- a/Chalice/tests/permission-model/predicates.output.txt +++ b/Chalice/tests/permission-model/predicates.output.txt @@ -4,6 +4,7 @@ Verification of predicates.chalice using parameters="" 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. +The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 28.3: The end of method b3 is unreachable. 49.3: The end of method b5 is unreachable. diff --git a/Chalice/tests/permission-model/sequences.output.txt b/Chalice/tests/permission-model/sequences.output.txt index f557b8c7..2cb8d25d 100644 --- a/Chalice/tests/permission-model/sequences.output.txt +++ b/Chalice/tests/permission-model/sequences.output.txt @@ -3,4 +3,5 @@ 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 +The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. Boogie program verifier finished with 2 errors and 0 smoke test warnings.
|