diff options
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.
|