1 files changed, 121 insertions, 0 deletions
diff --git a/Chalice/tests/general-tests/SmokeTestTest.chalice b/Chalice/tests/general-tests/SmokeTestTest.chalice
new file mode 100644
index 00000000..6ff283ec
--- /dev/null
+++ b/Chalice/tests/general-tests/SmokeTestTest.chalice
@@ -0,0 +1,121 @@
+// This file is meant as a test for Chalice's smoke testing feature (command line switch -smoke)
+class Cell {
+  var f: int;
+  
+  invariant acc(this.f) && f == 1
+  invariant f == 2 // SMOKE: contradiction
+  
+  method a1()
+    requires false // SMOKE: precondition is false
+  {}
+  
+  method a2()
+    requires acc(this.f,-2) // SMOKE: precondition is equivalent to false
+  {}
+  
+  method a3()
+    requires acc(this.f)
+  {
+    if (this.f > 0) {
+      this.f := 0;
+    }
+  }
+  
+  method a4()
+    requires acc(this.f)
+  {
+    if (false) {
+      this.f := 0; // SMOKE: unreachable
+    }
+  }
+  
+  method a5()
+    requires acc(this.f)
+  {
+    if (true) {
+      this.f := 0;
+    }
+  }
+  
+  method a6()
+    requires acc(this.f)
+  {
+    if (false) {
+      this.f := 0; // SMOKE: unreachable
+    } else {
+      this.f := 1;
+    }
+  }
+  
+  method a7(i: int, j: int)
+    requires i != j;
+  {
+    assume i == j; // SMOKE: introduces contradiction
+  }
+  
+  method a8()
+    requires acc(this.f)
+  {
+    while (true)
+      invariant acc(this.f)
+    {
+      this.f := this.f + 1
+    }
+    // SMOKE: unreachable, loop does not terminate
+  }
+  
+  method a9()
+    requires acc(this.f)
+  {
+    call a8()
+  }
+  
+  method a10()
+    requires acc(this.f)
+  {
+    if (true) {
+      this.f := 0;
+    } else {
+      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
+  }
+  
+  predicate valid {
+    1 == 2 // SMOKE: contradiction
+  }
+}
+
+channel C(msg: bool) where msg && !msg // SMOKE: contradiction
+\ No newline at end of file