From 2632156b2b42feeb119288afd4c462aa946b69e3 Mon Sep 17 00:00:00 2001
From: kyessenov <unknown>
Date: Fri, 3 Sep 2010 20:45:23 +0000
Subject: Chalice: incorporate another regression test

---
 Chalice/refinements/AngelicExec.chalice | 34 +++++++++++++++++++++++++++++++++
 Chalice/refinements/Answer              |  4 ++++
 Chalice/refinements/test.sh             |  1 +
 3 files changed, 39 insertions(+)
 create mode 100644 Chalice/refinements/AngelicExec.chalice

(limited to 'Chalice')

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
-- 
cgit v1.2.3