diff options
| author |  stefanheule <unknown> | 2012-09-20 11:34:50 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-09-20 11:34:50 +0200 |
| commit | f5a4ee5fb54f704387dcfdc7e4ee183d1bbc7876 (patch) | |
| tree | a3f62f3f79b6256946b717988b8ae0370399f06d | |
| parent | 071a2eae55d581e725a0bbd9a032b4c036b4b266 (diff) | |
Chalice: New regression tests for fixed workitems 10189 and 10208.
4 files changed, 76 insertions, 0 deletions
diff --git a/Chalice/tests/regressions/workitem-10189.chalice b/Chalice/tests/regressions/workitem-10189.chalice new file mode 100644 index 00000000..b37b83f2 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10189.chalice @@ -0,0 +1,23 @@ +class Node { + var v: int + var next: Node + + predicate V { + acc(v) + && acc(next) + && (next != null ==> next.V) + } + + unlimited function length(): int + requires rd(V) + { 1 + unfolding rd(V) in next == null ? 0 : next.length() } + + unlimited function at(i: int): int + requires rd(V) + requires i >= 0 + requires i < length() // XXXX + { + unfolding rd(V) in i == 0 ? v : next.at(i - 1) + // Precondition at XXX might not hold + } +}
\ No newline at end of file diff --git a/Chalice/tests/regressions/workitem-10189.output.txt b/Chalice/tests/regressions/workitem-10189.output.txt new file mode 100644 index 00000000..96f05468 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10189.output.txt @@ -0,0 +1,4 @@ +Verification of workitem-10189.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10208.chalice b/Chalice/tests/regressions/workitem-10208.chalice new file mode 100644 index 00000000..ae1a7d89 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10208.chalice @@ -0,0 +1,41 @@ +class Test {
+ var f1: int;
+ var f2: int;
+
+ predicate valid {
+ acc(f1) && acc(f2) && f1 == f2
+ }
+
+ method test()
+ requires valid
+ {
+ unfold valid
+ f1 := 2
+ f2 := 2
+ fold valid
+
+ /* --- not strictly necessary */
+ unfold valid
+ assert f1 == 2
+ fold valid
+ /* --- */
+
+ call test2()
+
+ unfold valid
+ assert f1 == 2 // BUG: this should not verify (1)
+ assert false // BUG: this should not verify (2)
+ }
+
+ method test2()
+ requires valid
+ ensures valid
+ ensures unfolding valid in f1 == 1 // line (1) above verifies also without this postcondition
+ {
+ unfold valid
+ f1 := 1
+ f2 := 1
+ fold valid
+ }
+
+}
diff --git a/Chalice/tests/regressions/workitem-10208.output.txt b/Chalice/tests/regressions/workitem-10208.output.txt new file mode 100644 index 00000000..0666393a --- /dev/null +++ b/Chalice/tests/regressions/workitem-10208.output.txt @@ -0,0 +1,8 @@ +Verification of workitem-10208.chalice using parameters=""
+
+ 26.5: Assertion might not hold. The expression at 26.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. + 9.3: The end of method test is unreachable. + +Boogie program verifier finished with 1 errors and 1 smoke test warnings
|