Chalice: Improve smoke testing: look for preconditions of functions, predicates and monitor invariants that are equivalent to false, and add a command line option "/smokeAll" to insert 'assert false' after *every* Chalice statement.

2 files changed, 25 insertions, 14 deletions

diff --git a/Chalice/tests/examples/SmokeTestTest.chalice b/Chalice/tests/examples/SmokeTestTest.chalice
index 2f32625e..44bba5da 100644
--- a/Chalice/tests/examples/SmokeTestTest.chalice
+++ b/Chalice/tests/examples/SmokeTestTest.chalice
@@ -2,6 +2,9 @@
 class Cell {

   var f: int;

   

+  invariant acc(this.f) && f == 1

+  invariant f == 2 // SMOKE: contradiction

+  

   method a1()

     requires false // SMOKE: precondition is false

   {}

@@ -109,4 +112,9 @@ class Cell {
   {

     call a13(); // SMOKE: statements afterwards not reachable anymore

   }

+  

+  predicate valid {

+    1 == 2 // SMOKE: contradiction

+  }

 }

+

diff --git a/Chalice/tests/examples/SmokeTestTest.output.txt b/Chalice/tests/examples/SmokeTestTest.output.txt
index 0d7985d6..697119cb 100644
--- a/Chalice/tests/examples/SmokeTestTest.output.txt
+++ b/Chalice/tests/examples/SmokeTestTest.output.txt
@@ -1,19 +1,22 @@
 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.
+  106.3: The postcondition at 107.13 might not hold. The expression at 107.13 might not evaluate to true.
 
 The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
-  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.
+  2.1: Monitor invariant is equivalent to false.
+  8.3: Precondition of method a1 is equivalent to false.
+  12.3: Precondition of method a2 is equivalent to false.
+  27.5: The begging of the if-branch is unreachable.
+  43.5: The begging of the if-branch is unreachable.
+  53.5: Assumption introduces a contradiction.
+  59.5: The statements after the while-loop are unreachable.
+  76.5: The begging of the else-branch is unreachable.
+  83.3: Precondition of function f1 is equivalent to false.
+  90.5: The begging of the if-branch is unreachable.
+  93.7: The begging of the else-branch is unreachable.
+  93.19: Assumption introduces a contradiction.
+  100.5: Assumption introduces a contradiction.
+  113.5: The statements after the method call statement are unreachable.
+  116.3: Predicate Cell.valid is equivalent to false.
 
-Boogie program verifier finished with 1 errors and 12 smoke test warnings.

+Boogie program verifier finished with 1 errors and 15 smoke test warnings.