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.

20 files changed, 87 insertions, 48 deletions

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.