diff options
| author |  stefanheule <unknown> | 2011-07-18 17:10:17 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-07-18 17:10:17 +0200 |
| commit | 10dc1b6325fd4445a972f4807948c0181942ea13 (patch) | |
| tree | 18114d503798633c81fe9cec29d432ab27f8b5b5 /Chalice/tests | |
| parent | 186b3e2e4a8b461212f9b97255b5f64d045df23f (diff) | |
Chalice: Smoke testing to find unreachable code, preconditions that are equivalent to false and assumptions that introduce contradictions. Can be used with the command line switch "-smoke".
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 +
|