diff options
| author |  stefanheule <unknown> | 2012-03-12 00:34:01 -0700 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-03-12 00:34:01 -0700 |
| commit | 15e84f942f531864005408a10d684f6f5bf784e4 (patch) | |
| tree | b256a2b9d8d2ffb67759759287aeb63406a1cb34 | |
| parent | 69c2322de145868daba6aba5277e8a571768e9d7 (diff) | |
Chalice: two new tests to check the predicate fix.
| -rw-r--r-- | Chalice/build.sbt | 2 | ||||
| -rw-r--r-- | Chalice/tests/predicates/setset.chalice | 57 | ||||
| -rw-r--r-- | Chalice/tests/predicates/setset.output.txt | 8 | ||||
| -rw-r--r-- | Chalice/tests/predicates/unfolding.chalice | 31 | ||||
| -rw-r--r-- | Chalice/tests/predicates/unfolding.output.txt | 5 |
5 files changed, 103 insertions, 0 deletions
diff --git a/Chalice/build.sbt b/Chalice/build.sbt index 65b12413..3fa72ec5 100644 --- a/Chalice/build.sbt +++ b/Chalice/build.sbt @@ -6,3 +6,5 @@ version := "1.0" scalaVersion := "2.8.1" scalacOptions += "-deprecation" + +libraryDependencies += "org.scalatest" %% "scalatest" % "1.7.1" % "test" diff --git a/Chalice/tests/predicates/setset.chalice b/Chalice/tests/predicates/setset.chalice new file mode 100644 index 00000000..512c65c1 --- /dev/null +++ b/Chalice/tests/predicates/setset.chalice @@ -0,0 +1,57 @@ +class Node {
+ var value: int;
+
+ method init(v: int)
+ requires acc(value)
+ ensures valid
+ {
+ value := v
+ fold this.valid
+ }
+
+ function get():int requires valid { unfolding valid in value }
+
+ method set(v: int)
+ requires valid
+ ensures valid && get() == v
+ {
+ unfold valid
+ value := v
+ fold valid
+ }
+
+ predicate valid {
+ acc(value)
+ }
+
+ method main(x: Node, y: Node)
+ requires x != null && y != null
+ requires x.valid && y.valid
+ {
+ call x.set(3)
+ call y.set(3)
+ call x.set(3)
+ call y.set(3)
+ call x.set(3)
+ call y.set(3)
+ call x.set(3)
+ unfold x.valid
+ x.value := 3
+ fold x.valid
+ call y.set(3)
+ call x.set(3)
+ call y.set(3)
+ unfold x.valid
+ x.value := 3
+ fold x.valid
+ unfold x.valid
+ x.value := 3
+ fold x.valid
+ call x.set(3)
+ call y.set(3)
+ call x.set(4)
+
+ assert y.get() == 3
+ assert x.get() == 3 // error: should fail
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/predicates/setset.output.txt b/Chalice/tests/predicates/setset.output.txt new file mode 100644 index 00000000..c20911f0 --- /dev/null +++ b/Chalice/tests/predicates/setset.output.txt @@ -0,0 +1,8 @@ +Verification of setset.chalice using parameters=""
+
+ 55.5: Assertion might not hold. The expression at 55.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. + 27.3: The end of method main is unreachable. + +Boogie program verifier finished with 1 errors and 1 smoke test warnings.
diff --git a/Chalice/tests/predicates/unfolding.chalice b/Chalice/tests/predicates/unfolding.chalice new file mode 100644 index 00000000..f01b237d --- /dev/null +++ b/Chalice/tests/predicates/unfolding.chalice @@ -0,0 +1,31 @@ +class Cell {
+ var value: int;
+
+ predicate p { acc(value) }
+
+ method test()
+ requires p
+ {
+ var tmp: int := unfolding p in value;
+ var tmp2: int := unfolding p in value;
+ call void()
+ assert tmp == unfolding p in value // ERROR: should fail
+ }
+
+ method test2()
+ requires p
+ {
+ var tmp: int := unfolding p in value;
+ var tmp2: int := unfolding p in value;
+ call v()
+ assert tmp == unfolding p in value
+ }
+
+ method v() requires true {}
+
+ method void()
+ requires p
+ ensures p
+ {}
+
+}
diff --git a/Chalice/tests/predicates/unfolding.output.txt b/Chalice/tests/predicates/unfolding.output.txt new file mode 100644 index 00000000..4a1ebbde --- /dev/null +++ b/Chalice/tests/predicates/unfolding.output.txt @@ -0,0 +1,5 @@ +Verification of unfolding.chalice using parameters=""
+
+ 12.5: Assertion might not hold. The expression at 12.12 might not evaluate to true. + +Boogie program verifier finished with 1 errors and 0 smoke test warnings.
|