diff options
Diffstat (limited to 'Chalice')
67 files changed, 455 insertions, 92 deletions
diff --git a/Chalice/tests/examples/ProdConsChannel.chalice b/Chalice/tests/examples/ProdConsChannel.chalice index 563d72b6..abac4f5c 100644 --- a/Chalice/tests/examples/ProdConsChannel.chalice +++ b/Chalice/tests/examples/ProdConsChannel.chalice @@ -42,85 +42,4 @@ class Program { receive c := ch
}
}
-
- // variations
- method Main0() { // error: debt remains after body
- var ch := new Ch
- fork tk0 := Producer(ch)
- fork tk1 := Consumer(ch)
- // join tk0
- join tk1
- }
- method Main1() {
- var ch := new Ch
- fork tk0 := Producer(ch)
- fork tk1 := Consumer(ch)
- join tk0
- // join tk1
- } // no problem
- method Producer0(ch: Ch) // error: debt remains after body
- requires ch != null
- ensures credit(ch)
- {
- var i := 0
- while (i < 25)
- {
- var x := i*i
- var c := new Cell { val := x }
- send ch(c)
- i := i + 1
- }
- // send ch(null)
- }
- method Producer1(ch: Ch)
- requires ch != null
- ensures credit(ch)
- {
- var i := 0
- while (i < 25)
- {
- var x := i*i
- var c := new Cell { val := x }
- send ch(c)
- i := i + 1 + c.val // error: can no longer read c.val
- }
- send ch(null)
- }
- method Consumer0(ch: Ch)
- requires rd(ch.mu) && waitlevel << ch.mu
- requires credit(ch)
- ensures rd(ch.mu)
- {
- var c: Cell
- receive c := ch
- while (c != null && c.val == 7) // this consumer may end early, but that's allowed
- invariant rd(ch.mu) && waitlevel << ch.mu
- invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)
- {
- var i := c.val
- receive c := ch
- }
- }
- method Consumer1(ch: Ch)
- requires rd(ch.mu) && waitlevel << ch.mu
- requires credit(ch)
- ensures rd(ch.mu)
- {
- var c: Cell
- receive c := ch
- if (c != null) {
- assert 0 <= c.val // follows from where clause
- }
- }
- method Consumer2(ch: Ch)
- requires rd(ch.mu) && waitlevel << ch.mu
- requires credit(ch)
- ensures rd(ch.mu)
- {
- var c: Cell
- receive c := ch
- if (c != null) {
- assert c.val < 2 // error: does not follow from where clause
- }
- }
}
diff --git a/Chalice/tests/examples/ProdConsChannel.output.txt b/Chalice/tests/examples/ProdConsChannel.output.txt index 167898fb..4d91605c 100644 --- a/Chalice/tests/examples/ProdConsChannel.output.txt +++ b/Chalice/tests/examples/ProdConsChannel.output.txt @@ -1,11 +1,4 @@ Verification of ProdConsChannel.chalice using parameters=""
- 47.3: Method body is not allowed to leave any debt. - 61.3: Method body is not allowed to leave any debt. - 85.20: Location might not be readable. - 123.7: Assertion might not hold. The expression at 123.14 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. - 80.5: The end of the while-loop is unreachable. - -Boogie program verifier finished with 4 errors and 1 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/examples/ImplicitLocals.chalice b/Chalice/tests/general-tests/ImplicitLocals.chalice index 15ebe8e0..15ebe8e0 100644 --- a/Chalice/tests/examples/ImplicitLocals.chalice +++ b/Chalice/tests/general-tests/ImplicitLocals.chalice diff --git a/Chalice/tests/examples/ImplicitLocals.output.txt b/Chalice/tests/general-tests/ImplicitLocals.output.txt index db26bba6..db26bba6 100644 --- a/Chalice/tests/examples/ImplicitLocals.output.txt +++ b/Chalice/tests/general-tests/ImplicitLocals.output.txt diff --git a/Chalice/tests/examples/LoopLockChange.chalice b/Chalice/tests/general-tests/LoopLockChange.chalice index 5ccce089..5ccce089 100644 --- a/Chalice/tests/examples/LoopLockChange.chalice +++ b/Chalice/tests/general-tests/LoopLockChange.chalice diff --git a/Chalice/tests/examples/LoopLockChange.output.txt b/Chalice/tests/general-tests/LoopLockChange.output.txt index 19e84f93..19e84f93 100644 --- a/Chalice/tests/examples/LoopLockChange.output.txt +++ b/Chalice/tests/general-tests/LoopLockChange.output.txt diff --git a/Chalice/tests/examples/RockBand-automagic.chalice b/Chalice/tests/general-tests/RockBand-automagic.chalice index 8a64b691..8a64b691 100644 --- a/Chalice/tests/examples/RockBand-automagic.chalice +++ b/Chalice/tests/general-tests/RockBand-automagic.chalice diff --git a/Chalice/tests/examples/RockBand-automagic.output.txt b/Chalice/tests/general-tests/RockBand-automagic.output.txt index 2e62b457..2e62b457 100644 --- a/Chalice/tests/examples/RockBand-automagic.output.txt +++ b/Chalice/tests/general-tests/RockBand-automagic.output.txt diff --git a/Chalice/tests/examples/SmokeTestTest.chalice b/Chalice/tests/general-tests/SmokeTestTest.chalice index 6ff283ec..6ff283ec 100644 --- a/Chalice/tests/examples/SmokeTestTest.chalice +++ b/Chalice/tests/general-tests/SmokeTestTest.chalice diff --git a/Chalice/tests/examples/SmokeTestTest.output.txt b/Chalice/tests/general-tests/SmokeTestTest.output.txt index 3d1cd786..3d1cd786 100644 --- a/Chalice/tests/examples/SmokeTestTest.output.txt +++ b/Chalice/tests/general-tests/SmokeTestTest.output.txt diff --git a/Chalice/tests/general-tests/VariationsOfProdConsChannel.chalice b/Chalice/tests/general-tests/VariationsOfProdConsChannel.chalice new file mode 100644 index 00000000..2d2f9b91 --- /dev/null +++ b/Chalice/tests/general-tests/VariationsOfProdConsChannel.chalice @@ -0,0 +1,88 @@ +class Cell {
+ var val: int
+}
+
+channel Ch(c: Cell) where
+ c != null ==> acc(c.val) && 0 <= c.val && credit(this)
+
+class Program {
+ method Main0() { // error: debt remains after body
+ var ch := new Ch
+ fork tk0 := Producer(ch)
+ fork tk1 := Consumer(ch)
+ // join tk0
+ join tk1
+ }
+ method Main1() {
+ var ch := new Ch
+ fork tk0 := Producer(ch)
+ fork tk1 := Consumer(ch)
+ join tk0
+ // join tk1
+ } // no problem
+ method Producer0(ch: Ch) // error: debt remains after body
+ requires ch != null
+ ensures credit(ch)
+ {
+ var i := 0
+ while (i < 25)
+ {
+ var x := i*i
+ var c := new Cell { val := x }
+ send ch(c)
+ i := i + 1
+ }
+ // send ch(null)
+ }
+ method Producer1(ch: Ch)
+ requires ch != null
+ ensures credit(ch)
+ {
+ var i := 0
+ while (i < 25)
+ {
+ var x := i*i
+ var c := new Cell { val := x }
+ send ch(c)
+ i := i + 1 + c.val // error: can no longer read c.val
+ }
+ send ch(null)
+ }
+ method Consumer0(ch: Ch)
+ requires rd(ch.mu) && waitlevel << ch.mu
+ requires credit(ch)
+ ensures rd(ch.mu)
+ {
+ var c: Cell
+ receive c := ch
+ while (c != null && c.val == 7) // this consumer may end early, but that's allowed
+ invariant rd(ch.mu) && waitlevel << ch.mu
+ invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)
+ {
+ var i := c.val
+ receive c := ch
+ }
+ }
+ method Consumer1(ch: Ch)
+ requires rd(ch.mu) && waitlevel << ch.mu
+ requires credit(ch)
+ ensures rd(ch.mu)
+ {
+ var c: Cell
+ receive c := ch
+ if (c != null) {
+ assert 0 <= c.val // follows from where clause
+ }
+ }
+ method Consumer2(ch: Ch)
+ requires rd(ch.mu) && waitlevel << ch.mu
+ requires credit(ch)
+ ensures rd(ch.mu)
+ {
+ var c: Cell
+ receive c := ch
+ if (c != null) {
+ assert c.val < 2 // error: does not follow from where clause
+ }
+ }
+}
diff --git a/Chalice/tests/general-tests/VariationsOfProdConsChannel.output.txt b/Chalice/tests/general-tests/VariationsOfProdConsChannel.output.txt new file mode 100644 index 00000000..d5b9c9ee --- /dev/null +++ b/Chalice/tests/general-tests/VariationsOfProdConsChannel.output.txt @@ -0,0 +1,13 @@ +Verification of VariationsOfProdConsChannel.chalice using parameters=""
+
+The program did not typecheck.
+11.5: call of undeclared member Producer in class Program
+<undefined position>: Invalid token type. Program does not declare a method Producer.
+12.5: call of undeclared member Consumer in class Program
+<undefined position>: Invalid token type. Program does not declare a method Consumer.
+14.10: the first argument of a join async must be a token
+18.5: call of undeclared member Producer in class Program
+<undefined position>: Invalid token type. Program does not declare a method Producer.
+19.5: call of undeclared member Consumer in class Program
+<undefined position>: Invalid token type. Program does not declare a method Consumer.
+20.10: the first argument of a join async must be a token
diff --git a/Chalice/tests/examples/cell-defaults.chalice b/Chalice/tests/general-tests/cell-defaults.chalice index eb826f89..eb826f89 100644 --- a/Chalice/tests/examples/cell-defaults.chalice +++ b/Chalice/tests/general-tests/cell-defaults.chalice diff --git a/Chalice/tests/examples/cell-defaults.output.txt b/Chalice/tests/general-tests/cell-defaults.output.txt index 138a5717..138a5717 100644 --- a/Chalice/tests/examples/cell-defaults.output.txt +++ b/Chalice/tests/general-tests/cell-defaults.output.txt diff --git a/Chalice/tests/examples/counter.chalice b/Chalice/tests/general-tests/counter.chalice index 828cf005..828cf005 100644 --- a/Chalice/tests/examples/counter.chalice +++ b/Chalice/tests/general-tests/counter.chalice diff --git a/Chalice/tests/examples/counter.output.txt b/Chalice/tests/general-tests/counter.output.txt index 1d5be0ea..1d5be0ea 100644 --- a/Chalice/tests/examples/counter.output.txt +++ b/Chalice/tests/general-tests/counter.output.txt diff --git a/Chalice/tests/general-tests/generate_reference.bat b/Chalice/tests/general-tests/generate_reference.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/general-tests/generate_reference.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/general-tests/generate_reference_all.bat b/Chalice/tests/general-tests/generate_reference_all.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/general-tests/generate_reference_all.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/examples/prog0.chalice b/Chalice/tests/general-tests/prog0.chalice index fb835a24..fb835a24 100644 --- a/Chalice/tests/examples/prog0.chalice +++ b/Chalice/tests/general-tests/prog0.chalice diff --git a/Chalice/tests/examples/prog0.output.txt b/Chalice/tests/general-tests/prog0.output.txt index 5b329874..5b329874 100644 --- a/Chalice/tests/examples/prog0.output.txt +++ b/Chalice/tests/general-tests/prog0.output.txt diff --git a/Chalice/tests/examples/prog1.chalice b/Chalice/tests/general-tests/prog1.chalice index 133de36d..133de36d 100644 --- a/Chalice/tests/examples/prog1.chalice +++ b/Chalice/tests/general-tests/prog1.chalice diff --git a/Chalice/tests/examples/prog1.output.txt b/Chalice/tests/general-tests/prog1.output.txt index 630ecdfa..630ecdfa 100644 --- a/Chalice/tests/examples/prog1.output.txt +++ b/Chalice/tests/general-tests/prog1.output.txt diff --git a/Chalice/tests/examples/prog2.chalice b/Chalice/tests/general-tests/prog2.chalice index 55fe8ff5..55fe8ff5 100644 --- a/Chalice/tests/examples/prog2.chalice +++ b/Chalice/tests/general-tests/prog2.chalice diff --git a/Chalice/tests/examples/prog2.output.txt b/Chalice/tests/general-tests/prog2.output.txt index b9d88bbe..b9d88bbe 100644 --- a/Chalice/tests/examples/prog2.output.txt +++ b/Chalice/tests/general-tests/prog2.output.txt diff --git a/Chalice/tests/examples/prog3.chalice b/Chalice/tests/general-tests/prog3.chalice index de5dfad7..de5dfad7 100644 --- a/Chalice/tests/examples/prog3.chalice +++ b/Chalice/tests/general-tests/prog3.chalice diff --git a/Chalice/tests/examples/prog3.output.txt b/Chalice/tests/general-tests/prog3.output.txt index 18d05658..18d05658 100644 --- a/Chalice/tests/examples/prog3.output.txt +++ b/Chalice/tests/general-tests/prog3.output.txt diff --git a/Chalice/tests/examples/prog4.chalice b/Chalice/tests/general-tests/prog4.chalice index 3c655c71..3c655c71 100644 --- a/Chalice/tests/examples/prog4.chalice +++ b/Chalice/tests/general-tests/prog4.chalice diff --git a/Chalice/tests/examples/prog4.output.txt b/Chalice/tests/general-tests/prog4.output.txt index 9415df7c..9415df7c 100644 --- a/Chalice/tests/examples/prog4.output.txt +++ b/Chalice/tests/general-tests/prog4.output.txt diff --git a/Chalice/tests/examples/quantifiers.chalice b/Chalice/tests/general-tests/quantifiers.chalice index 7377ca3f..7377ca3f 100644 --- a/Chalice/tests/examples/quantifiers.chalice +++ b/Chalice/tests/general-tests/quantifiers.chalice diff --git a/Chalice/tests/examples/quantifiers.output.txt b/Chalice/tests/general-tests/quantifiers.output.txt index 2f325c42..2f325c42 100644 --- a/Chalice/tests/examples/quantifiers.output.txt +++ b/Chalice/tests/general-tests/quantifiers.output.txt diff --git a/Chalice/tests/general-tests/reg_test.bat b/Chalice/tests/general-tests/reg_test.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/general-tests/reg_test.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/general-tests/reg_test_all.bat b/Chalice/tests/general-tests/reg_test_all.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/general-tests/reg_test_all.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/general-tests/test.bat b/Chalice/tests/general-tests/test.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/general-tests/test.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/readme.txt b/Chalice/tests/readme.txt index be0b6f91..d6875825 100644 --- a/Chalice/tests/readme.txt +++ b/Chalice/tests/readme.txt @@ -5,8 +5,13 @@ Chalice Test Suite Contents
--------
- examples: Various examples how Chalice can be used to verify concurrent
- programs.
-- permission-model: Regression tests for the permission model of Chalice.
+ programs. These tests represent (the core of) real problems and are therefore
+ well suited for performance and comparison tests (e.g. with other tools).
+- general-tests: Regression tests for various aspects of Chalice.
+- regressions: Regression tests for fixed bugs to ensure they do not occur
+ again.
+- permission-model: Regression tests specifically for the permission model of
+ Chalice.
- refinements: Regression tests for the refinement extension.
- test-scripts: Some batch scripts that can be used to execute the tests in an
easy and automated way. More information below.
@@ -19,6 +24,7 @@ tests in different ways. There are launchers in the test directories (e.g. in examples or permission-model) to access them.
Commands (sorted by relevance):
+- runalltests.bat: Executes all tests in all test folders.
- test.bat <file> [-params]: Execute a test and output the result of the
verification. Note: <file> must not include the file extension.
- reg_test.bat <file> [-params]: Execute a tests as a regression test, i.e., run
diff --git a/Chalice/tests/regressions/generate_reference.bat b/Chalice/tests/regressions/generate_reference.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/regressions/generate_reference.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/regressions/generate_reference_all.bat b/Chalice/tests/regressions/generate_reference_all.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/regressions/generate_reference_all.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/regressions/reg_test.bat b/Chalice/tests/regressions/reg_test.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/regressions/reg_test.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/regressions/reg_test_all.bat b/Chalice/tests/regressions/reg_test_all.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/regressions/reg_test_all.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/regressions/test.bat b/Chalice/tests/regressions/test.bat new file mode 100644 index 00000000..6864843c --- /dev/null +++ b/Chalice/tests/regressions/test.bat @@ -0,0 +1,2 @@ +@echo off
+call "..\test-scripts\%0" %*
diff --git a/Chalice/tests/regressions/workitem-10147.chalice b/Chalice/tests/regressions/workitem-10147.chalice new file mode 100644 index 00000000..eb6f31c7 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10147.chalice @@ -0,0 +1,22 @@ +class Cell {
+
+ var x: int;
+
+ // the declaration of a method with the same name for a parameter
+ // as well as a result alone does not yet cause a problem, but ...
+ method problematic_method(c: Cell) returns (c: Cell)
+ requires acc(c.x);
+ {
+ }
+
+ // ... calling it leads to various 'undeclared identifier' errors
+ // in boogie. (previously. now fixed by not allowing c as both in and out parameter)
+ method error()
+ {
+ var a: Cell := new Cell;
+ var b: Cell;
+
+ call b := problematic_method(a);
+ }
+
+}
diff --git a/Chalice/tests/regressions/workitem-10147.output.txt b/Chalice/tests/regressions/workitem-10147.output.txt new file mode 100644 index 00000000..63bb3c9c --- /dev/null +++ b/Chalice/tests/regressions/workitem-10147.output.txt @@ -0,0 +1,4 @@ +Verification of workitem-10147.chalice using parameters=""
+
+The program did not typecheck.
+7.3: duplicate parameter c of method problematic_method in class Cell
diff --git a/Chalice/tests/regressions/workitem-10190.chalice b/Chalice/tests/regressions/workitem-10190.chalice new file mode 100644 index 00000000..ad84553a --- /dev/null +++ b/Chalice/tests/regressions/workitem-10190.chalice @@ -0,0 +1,6 @@ +// previously resulted in a StackOverFlowError of the Chalice parser +class Node { +/* +Lorem ipsum dolor sit amet, consetetur sadipscing elitr, sed diam nonumy eirmod tempor invidunt ut labore et dolore magna aliquyam erat, sed diam voluptua. At vero eos et accusam et justo duo dolores et ea rebum. Stet clita kasd gubergren, no sea takimata sanctus est Lorem ipsum dolor sit amet. Lorem ipsum dolor sit amet, consetetur sadipscing elitr, sed diam nonumy eirmod tempor invidunt ut labore et dolore magna aliquyam erat, sed diam voluptua. +*/ +}
\ No newline at end of file diff --git a/Chalice/tests/regressions/workitem-10190.output.txt b/Chalice/tests/regressions/workitem-10190.output.txt new file mode 100644 index 00000000..e314cbd3 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10190.output.txt @@ -0,0 +1,5 @@ +Verification of workitem-10190.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 verified, 1 error +
diff --git a/Chalice/tests/regressions/workitem-10192.chalice b/Chalice/tests/regressions/workitem-10192.chalice new file mode 100644 index 00000000..06ff5881 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10192.chalice @@ -0,0 +1,19 @@ +class Sequences { + var xs: seq<int> + + method append(a: int) + requires acc(xs) + ensures acc(xs) + ensures size() == old(size()) + 1 /* verifies */ + ensures |xs| == old(|xs|) + 1 /* previously failed */ + { xs := xs ++ [a] } + + /* this heap-independent version also verifies. */ + method append0(ins: seq<int>, a: int) returns (outs: seq<int>) + ensures |outs| == |ins| + 1 + { outs := ins ++ [a] } + + function size(): int + requires rd(xs) + { |xs| } +} diff --git a/Chalice/tests/regressions/workitem-10192.output.txt b/Chalice/tests/regressions/workitem-10192.output.txt new file mode 100644 index 00000000..1f5fbeec --- /dev/null +++ b/Chalice/tests/regressions/workitem-10192.output.txt @@ -0,0 +1,4 @@ +Verification of workitem-10192.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/regressions/workitem-10194.chalice b/Chalice/tests/regressions/workitem-10194.chalice new file mode 100644 index 00000000..5828b0bf --- /dev/null +++ b/Chalice/tests/regressions/workitem-10194.chalice @@ -0,0 +1,37 @@ +class Test { + var x: int + var tk: token<Test.incX> + + predicate V { acc(x) } + + method incX() + requires V + ensures V + { + unfold V + x := x + 1 + fold V + } + + method joinTk() + requires acc(tk) && tk != null && acc(tk.joinable) && tk.joinable + requires eval(tk.fork this.incX(), true) + ensures V + ensures unfolding V in x == old(x) // ERROR: old(x) is not readable (no error here, previously) + { + join tk + assert V + } + + method test() + requires acc(x) && x == 0 + requires acc(tk) + { + fold V + fork tklocal := incX() + tk := tklocal + call joinTk() + unfold V + assert x == old(x) // this verified previously (without any errors anywhere in the file) + } +}
\ No newline at end of file diff --git a/Chalice/tests/regressions/workitem-10194.output.txt b/Chalice/tests/regressions/workitem-10194.output.txt new file mode 100644 index 00000000..3ed31c08 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10194.output.txt @@ -0,0 +1,5 @@ +Verification of workitem-10194.chalice using parameters=""
+
+ 20.35: Location might not be readable. + +Boogie program verifier finished with 1 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/regressions/workitem-10195.chalice b/Chalice/tests/regressions/workitem-10195.chalice new file mode 100644 index 00000000..99ea69f8 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10195.chalice @@ -0,0 +1,38 @@ +class Test { + method fails() + { + assert forall j in [10..5] :: true // ERROR: min > max + assert false // failed previously, now we get a smoke warning + } + + method succeeds1() + { + assert forall j in [10..5] :: f(j) == 0 // ERROR: min > max + assert false // failed previously, now we get a smoke warning + } + + method fails1() + { + assert forall j in [5..10] :: f(j) == 0 + } + + method succeeds2(a: int, b: int) + requires 0 <= a && 0 <= b + requires f(a) < f(b) + { + assert forall j in [f(b)..f(a)] :: f(j) == 0 // ERROR: min > max + assert false // holds + } + + method fails2(a: int, b: int) + requires 0 <= a && 0 <= b + requires 0 < f(a) + requires f(a) < f(b) + { + assert forall j in [f(a)..f(b)] :: f(j) == 0 + } + + function f(i: int): int + requires 0 <= i + { 0 } + }
\ No newline at end of file diff --git a/Chalice/tests/regressions/workitem-10195.output.txt b/Chalice/tests/regressions/workitem-10195.output.txt new file mode 100644 index 00000000..0636df17 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10195.output.txt @@ -0,0 +1,12 @@ +Verification of workitem-10195.chalice using parameters=""
+
+ 4.14: Range minimum might not be smaller or equal to range maximum. + 10.14: Range minimum might not be smaller or equal to range maximum. + +The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. + 2.5: The end of method fails is unreachable. + 8.5: The end of method succeeds1 is unreachable. + 19.9: Precondition of method succeeds2 is equivalent to false. + 27.9: Precondition of method fails2 is equivalent to false. + +Boogie program verifier finished with 2 errors and 4 smoke test warnings.
diff --git a/Chalice/tests/regressions/workitem-10196.chalice b/Chalice/tests/regressions/workitem-10196.chalice new file mode 100644 index 00000000..9257e5c2 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10196.chalice @@ -0,0 +1,11 @@ +class C { + method singleWarning() + { assert forall i in [] :: true } // previously, quantification over the empty list resulted in Boogie errors + + method multipleWarnings() + { assert forall i in [] :: reqIGt0(i) == i } // previously, quantification over the empty list resulted in Boogie errors + + function reqIGt0(i: int): int + requires i >= 0 + { i } +}
\ No newline at end of file diff --git a/Chalice/tests/regressions/workitem-10196.output.txt b/Chalice/tests/regressions/workitem-10196.output.txt new file mode 100644 index 00000000..013880cc --- /dev/null +++ b/Chalice/tests/regressions/workitem-10196.output.txt @@ -0,0 +1,4 @@ +Verification of workitem-10196.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/regressions/workitem-10197.chalice b/Chalice/tests/regressions/workitem-10197.chalice new file mode 100644 index 00000000..7212581c --- /dev/null +++ b/Chalice/tests/regressions/workitem-10197.chalice @@ -0,0 +1,7 @@ +class Cell { var x: int } + +class Test { + method noop() + ensures old(waitlevel) == waitlevel // previously resulted in Boogie errors + {} +}
\ No newline at end of file diff --git a/Chalice/tests/regressions/workitem-10197.output.txt b/Chalice/tests/regressions/workitem-10197.output.txt new file mode 100644 index 00000000..9cc1319a --- /dev/null +++ b/Chalice/tests/regressions/workitem-10197.output.txt @@ -0,0 +1,4 @@ +Verification of workitem-10197.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/regressions/workitem-10198.chalice b/Chalice/tests/regressions/workitem-10198.chalice new file mode 100644 index 00000000..fd51977d --- /dev/null +++ b/Chalice/tests/regressions/workitem-10198.chalice @@ -0,0 +1,17 @@ +class Cell { var x: int } + +class Test { + method get() returns (c: Cell) + ensures c != null + lockchange c /* previosly, this introduced errors */ + { + c := new Cell + } + + /* method was needed to get Boogie errors */ + method testRd() // expected ERROR: method might lock/unlock more than allowed + { + var x: Cell + call x := get() + } +}
\ No newline at end of file diff --git a/Chalice/tests/regressions/workitem-10198.output.txt b/Chalice/tests/regressions/workitem-10198.output.txt new file mode 100644 index 00000000..8e421059 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10198.output.txt @@ -0,0 +1,5 @@ +Verification of workitem-10198.chalice using parameters=""
+
+ 12.2: Method might lock/unlock more than allowed. + +Boogie program verifier finished with 1 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/regressions/workitem-10199.chalice b/Chalice/tests/regressions/workitem-10199.chalice new file mode 100644 index 00000000..678ed078 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10199.chalice @@ -0,0 +1,21 @@ +class Test { + var z: int + + predicate Z { acc(z) } + predicate ZZ { Z } // XXX + + method useZZ() + requires ZZ + { + // (ZZ,100) + unfold acc(ZZ, 40) + // (ZZ, 60), (Z, 40) + unfold acc(Z, 20) + // (ZZ, 60), (Z, 20), (z, 20) + fold acc(Z, 10) + // (ZZ, 60), (Z, 30), (z, 10) + fold acc(ZZ, 30) + // previoulsy: Fold might fail because the definition of Test.ZZ does not hold. Insufficient fraction at XXX for Test.Z. + // Should be (ZZ, 90), (z, 10) + } +}
\ No newline at end of file diff --git a/Chalice/tests/regressions/workitem-10199.output.txt b/Chalice/tests/regressions/workitem-10199.output.txt new file mode 100644 index 00000000..4fb873e7 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10199.output.txt @@ -0,0 +1,4 @@ +Verification of workitem-10199.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/regressions/workitem-10200.chalice b/Chalice/tests/regressions/workitem-10200.chalice new file mode 100644 index 00000000..a7394793 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10200.chalice @@ -0,0 +1,25 @@ +class Test { + var f: int; + + function fib(n: int): int + requires n >= 0 + { + n < 2 ? n : fib(n - 1) + fib(n - 2) // incompletness: termination not atomatically proven + } + + method fibSeq(n: int) returns (r: int) + requires n >= 0 + requires acc(this.f) + ensures acc(this.f) + ensures r == fib(n) // previous error: the postcondition might not hold + { + if (n < 2) { + r := n + } else { + var f1: int; var f2: int + call f1 := fibSeq(n - 1) + call f2 := fibSeq(n - 2) + r := f1 + f2 + } + } +}
\ No newline at end of file diff --git a/Chalice/tests/regressions/workitem-10200.output.txt b/Chalice/tests/regressions/workitem-10200.output.txt new file mode 100644 index 00000000..cac4bb62 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10200.output.txt @@ -0,0 +1,5 @@ +Verification of workitem-10200.chalice using parameters=""
+
+ 7.15: The heap of the callee might not be strictly smaller than the heap of the caller. + +Boogie program verifier finished with 1 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/regressions/workitem-8234.chalice b/Chalice/tests/regressions/workitem-8234.chalice new file mode 100644 index 00000000..5fbcea02 --- /dev/null +++ b/Chalice/tests/regressions/workitem-8234.chalice @@ -0,0 +1,26 @@ +class Test{
+ var tests : seq<Test>;
+ var total : int;
+
+ invariant acc(tests, 100);
+ invariant acc(total, 50);
+
+ function at(loc : int) : Test
+ requires acc(tests);
+ requires loc >= 0 && loc < size();
+ {
+ tests[loc]
+ }
+
+
+ function size() : int
+ requires acc(tests);
+ ensures result >= 0;
+ ensures result == |tests|; // previously, there was a nullpointer exception here
+ {
+ |tests|
+ }
+
+ predicate pre
+ { acc(total, 50) }
+}
\ No newline at end of file diff --git a/Chalice/tests/regressions/workitem-8234.output.txt b/Chalice/tests/regressions/workitem-8234.output.txt new file mode 100644 index 00000000..8d13e17a --- /dev/null +++ b/Chalice/tests/regressions/workitem-8234.output.txt @@ -0,0 +1,4 @@ +Verification of workitem-8234.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/regressions/workitem-8236.chalice b/Chalice/tests/regressions/workitem-8236.chalice new file mode 100644 index 00000000..819bdb74 --- /dev/null +++ b/Chalice/tests/regressions/workitem-8236.chalice @@ -0,0 +1,16 @@ +class Bug{
+
+ method Main() // expected ERROR: method might lock/unlock more than allowed
+ {
+ var a : Bug;
+ call a:= m();
+ }
+
+ method m() returns (a : Bug)
+ lockchange a // resulted previously in Boogie errors
+ {
+ a := new Bug;
+ share a;
+ acquire a;
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/regressions/workitem-8236.output.txt b/Chalice/tests/regressions/workitem-8236.output.txt new file mode 100644 index 00000000..30b42ab1 --- /dev/null +++ b/Chalice/tests/regressions/workitem-8236.output.txt @@ -0,0 +1,5 @@ +Verification of workitem-8236.chalice using parameters=""
+
+ 3.2: Method might lock/unlock more than allowed. + +Boogie program verifier finished with 1 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/regressions/workitem-9978.chalice b/Chalice/tests/regressions/workitem-9978.chalice new file mode 100644 index 00000000..02cd2e66 --- /dev/null +++ b/Chalice/tests/regressions/workitem-9978.chalice @@ -0,0 +1,9 @@ +class C {
+ method nullPointerException()
+ {
+ while (true)
+ {
+ fork nullPointerException(); // previously, fork without token inside a while loop introduced a nullpointer exception.
+ }
+ }
+}
diff --git a/Chalice/tests/regressions/workitem-9978.output.txt b/Chalice/tests/regressions/workitem-9978.output.txt new file mode 100644 index 00000000..0e557a3b --- /dev/null +++ b/Chalice/tests/regressions/workitem-9978.output.txt @@ -0,0 +1,6 @@ +Verification of workitem-9978.chalice using parameters=""
+
+ + 4.5: The statements after the while-loop are unreachable. + +Boogie program verifier finished with 0 errors and 1 smoke test warnings.
diff --git a/Chalice/tests/runalltests.bat b/Chalice/tests/runalltests.bat index 3b0df4a4..f391b1f9 100644 --- a/Chalice/tests/runalltests.bat +++ b/Chalice/tests/runalltests.bat @@ -11,7 +11,7 @@ if "%1"=="-no-summary" ( set t=0
set c=0
-for %%f in (examples permission-model) do (
+for %%f in (examples permission-model general-tests regressions) do (
echo Running tests in %%f ...
echo ------------------------------------------------------
cd %%f
diff --git a/Chalice/tests/test-scripts/readme.txt b/Chalice/tests/test-scripts/readme.txt new file mode 100644 index 00000000..d4f408e8 --- /dev/null +++ b/Chalice/tests/test-scripts/readme.txt @@ -0,0 +1,3 @@ +
+The scripts in this directory are NOT meant for direct execution, but rather
+provide the implementation of the same-named scripts in the actual test folders.
|