diff options
| author |  kyessenov <unknown> | 2010-09-03 20:45:23 +0000 |
|---|---|---|
| committer | kyessenov <unknown> | 2010-09-03 20:45:23 +0000 |
| commit | 2632156b2b42feeb119288afd4c462aa946b69e3 (patch) | |
| tree | 3eeb7137e876f743bdd6be06e6a7b86855e1dcc6 /Chalice | |
| parent | fa7f754906cd45425c6d4d695e5978f21d333e86 (diff) | |
Chalice: incorporate another regression test
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/refinements/AngelicExec.chalice | 34 | ||||
| -rw-r--r-- | Chalice/refinements/Answer | 4 | ||||
| -rw-r--r-- | Chalice/refinements/test.sh | 1 |
3 files changed, 39 insertions, 0 deletions
diff --git a/Chalice/refinements/AngelicExec.chalice b/Chalice/refinements/AngelicExec.chalice new file mode 100644 index 00000000..06ab9c83 --- /dev/null +++ b/Chalice/refinements/AngelicExec.chalice @@ -0,0 +1,34 @@ +class A0 {
+ method m(b: bool) {
+ var x;
+ if (b) {
+ var x [0 <= x && x < 3];
+ } else {
+ x := 1;
+ }
+ }
+}
+
+class B0 refines A0 {
+ refines m(b: bool) {
+ var x := 1;
+ }
+}
+
+class A1 refines A0 {
+ transforms m(b: bool) {
+ _
+ if {
+ replaces * by {x := 1;}
+ } else {
+ *
+ }
+ _
+ }
+}
+
+class A2 refines A1 {
+ refines m(b: bool) {
+ var x := 1;
+ }
+}
diff --git a/Chalice/refinements/Answer b/Chalice/refinements/Answer index a6654fc2..42767bfd 100644 --- a/Chalice/refinements/Answer +++ b/Chalice/refinements/Answer @@ -38,3 +38,7 @@ Boogie program verifier finished with 17 verified, 3 errors Processing Calculator.chalice Boogie program verifier finished with 15 verified, 0 errors
+Processing AngelicExec.chalice + 14.5: Refinement may produce different value for a declared local variable: x
+
+Boogie program verifier finished with 11 verified, 1 error
diff --git a/Chalice/refinements/test.sh b/Chalice/refinements/test.sh index 80b42258..8ebef27a 100644 --- a/Chalice/refinements/test.sh +++ b/Chalice/refinements/test.sh @@ -15,6 +15,7 @@ TESTS=" Pick.chalice TestCoupling.chalice Calculator.chalice + AngelicExec.chalice " # Switch to test directory |