diff options
Diffstat (limited to 'Chalice/tests')
-rw-r--r-- | Chalice/tests/examples/SmokeTestTest.chalice | 76 | ||||
-rw-r--r-- | Chalice/tests/examples/SmokeTestTest.output.txt | 15 |
2 files changed, 91 insertions, 0 deletions
diff --git a/Chalice/tests/examples/SmokeTestTest.chalice b/Chalice/tests/examples/SmokeTestTest.chalice new file mode 100644 index 00000000..a9bbf197 --- /dev/null +++ b/Chalice/tests/examples/SmokeTestTest.chalice @@ -0,0 +1,76 @@ +// 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;
+
+ method a1()
+ requires false
+ {}
+
+ method a2()
+ requires acc(this.f,-2)
+ {}
+
+ method a3()
+ requires acc(this.f)
+ {
+ if (this.f > 0) {
+ this.f := 0;
+ }
+ }
+
+ method a4()
+ requires acc(this.f)
+ {
+ if (false) {
+ this.f := 0;
+ }
+ }
+
+ method a5()
+ requires acc(this.f)
+ {
+ if (true) {
+ this.f := 0;
+ }
+ }
+
+ method a6()
+ requires acc(this.f)
+ {
+ if (false) {
+ this.f := 0;
+ } else {
+ this.f := 1;
+ }
+ }
+
+ method a7(i: int, j: int)
+ requires i != j;
+ {
+ assume i == j;
+ }
+
+ method a8()
+ requires acc(this.f)
+ {
+ while (true) {
+ this.f := this.f + 1
+ }
+ }
+
+ method a9()
+ {
+ call a8()
+ }
+
+ method a10()
+ requires acc(this.f)
+ {
+ if (true) {
+ this.f := 0;
+ } else {
+ this.f := 1;
+ }
+ }
+}
diff --git a/Chalice/tests/examples/SmokeTestTest.output.txt b/Chalice/tests/examples/SmokeTestTest.output.txt new file mode 100644 index 00000000..1fe23f64 --- /dev/null +++ b/Chalice/tests/examples/SmokeTestTest.output.txt @@ -0,0 +1,15 @@ +Verification of SmokeTestTest.chalice using parameters="-smoke"
+
+ 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. + 70.5: The end of the else-branch is unreachable. + +Smoke testing finished with 3 verified, 10 warnings +
|