From ea4e92df259713b79973a9d0bacebb09fb95fb57 Mon Sep 17 00:00:00 2001
From: kyessenov <unknown>
Date: Tue, 5 Oct 2010 01:26:01 +0000
Subject: Chalice: fix a bug where output variables of a method were not
 decoupled.

---
 Chalice/refinements/Answer              | 65 +++++++++++++++++----------------
 Chalice/refinements/TestRefines.chalice | 19 +++++++++-
 Chalice/src/Ast.scala                   |  9 ++++-
 Chalice/src/Resolver.scala              |  2 +-
 4 files changed, 59 insertions(+), 36 deletions(-)

(limited to 'Chalice')

diff --git a/Chalice/refinements/Answer b/Chalice/refinements/Answer
index 42767bfd..8bd8a24b 100644
--- a/Chalice/refinements/Answer
+++ b/Chalice/refinements/Answer
@@ -1,44 +1,45 @@
 Processing LoopSqRoot.chalice
-
-Boogie program verifier finished with 9 verified, 0 errors
+
+Boogie program verifier finished with 9 verified, 0 errors
 Processing RecSqRoot.chalice
-
-Boogie program verifier finished with 11 verified, 0 errors
+
+Boogie program verifier finished with 11 verified, 0 errors
 Processing SpecStmt.chalice
-  12.5: Assertion might not hold. The expression at 12.12 might not evaluate to true.
-  25.5: Assertion might not hold. The expression at 25.12 might not evaluate to true.
-  33.5: Assertion might not hold. The expression at 33.12 might not evaluate to true.
-
-Boogie program verifier finished with 4 verified, 3 errors
+  12.5: Assertion might not hold. The expression at 12.12 might not evaluate to true.
+  25.5: Assertion might not hold. The expression at 25.12 might not evaluate to true.
+  33.5: Assertion might not hold. The expression at 33.12 might not evaluate to true.
+
+Boogie program verifier finished with 4 verified, 3 errors
 Processing SumCubes.chalice
-
-Boogie program verifier finished with 6 verified, 0 errors
+
+Boogie program verifier finished with 6 verified, 0 errors
 Processing TestTransform.chalice
-
-Boogie program verifier finished with 10 verified, 0 errors
+
+Boogie program verifier finished with 10 verified, 0 errors
 Processing TestRefines.chalice
-
-Boogie program verifier finished with 9 verified, 0 errors
+  28.5: Refinement may produce different value for pre-state local variable: c
+
+Boogie program verifier finished with 14 verified, 1 error
 Processing RecFiniteDiff.chalice
-
-Boogie program verifier finished with 9 verified, 0 errors
+
+Boogie program verifier finished with 9 verified, 0 errors
 Processing LoopFiniteDiff.chalice
-
-Boogie program verifier finished with 12 verified, 0 errors
+
+Boogie program verifier finished with 12 verified, 0 errors
 Processing Pick.chalice
-  26.25: Sequence index might be larger than or equal to the length of the sequence.
-
-Boogie program verifier finished with 11 verified, 1 error
+  26.25: Sequence index might be larger than or equal to the length of the sequence.
+
+Boogie program verifier finished with 11 verified, 1 error
 Processing TestCoupling.chalice
-  35.13: The postcondition at 35.13 might not hold. Insufficient fraction at 35.13 for A1.y.
-  62.38: Location might not be readable.
-  66.5: Location might not be writable
-
-Boogie program verifier finished with 17 verified, 3 errors
+  35.13: The postcondition at 35.13 might not hold. Insufficient fraction at 35.13 for A1.y.
+  62.38: Location might not be readable.
+  66.5: Location might not be writable
+
+Boogie program verifier finished with 17 verified, 3 errors
 Processing Calculator.chalice
-
-Boogie program verifier finished with 15 verified, 0 errors
+
+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
+  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/TestRefines.chalice b/Chalice/refinements/TestRefines.chalice
index 2cfc19b2..3081eb90 100644
--- a/Chalice/refinements/TestRefines.chalice
+++ b/Chalice/refinements/TestRefines.chalice
@@ -9,5 +9,22 @@ class A {
 class B refines C {}
 class C refines D {}
 class D refines A {
-  transforms m(i:int) returns (j:int, k:int) {*} 
+  transforms m(i:int) returns (j:int, k:int) 
+  {
+  *
+  } 
+}
+
+class X {
+  method m() returns (c: bool) 
+  {
+    c := true;
+  }
+}
+
+class Y refines X {
+  refines m() returns (c: bool, d: bool)
+  {
+    c := false;
+  }
 }
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index edeb52ba..bd524ec3 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -260,11 +260,16 @@ case class SeqPat(pats: List[Transform]) extends Transform {
 case class RefinementBlock(con: List[Statement], abs: List[Statement]) extends Statement {
   if (con.size > 0) pos = con.first.pos
   // local variables in context at the beginning of the block
+
   var before: List[Variable] = null
   // shared declared local variables (mapping between abstract and concrete)
+  // should be called after resolution
   lazy val during: (List[Variable], List[Variable]) = {
-    val a = for (v <- abs.flatMap(s => s.Declares)) yield v;
-    val c = for (v <- a) yield con.flatMap(s => s.Declares).find(_ == v).get
+    val a = abs.flatMap(s => s.Declares);
+    val c = for (v <- a) yield con.flatMap(s => s.Declares).find(_ == v) match {
+      case Some(w) => w;
+      case None => v;
+    }
     (a,c)
   }         
   override def Declares = con flatMap {_.Declares}
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 7ccfe7e3..0c4ae979 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -1127,7 +1127,7 @@ object Resolver {
        }
      }
    }
-   resolveBody(mt.body, context.SetClass(mt.Parent).SetMember(mt), Nil)
+   resolveBody(mt.body, context.SetClass(mt.Parent).SetMember(mt), mt.refines.Outs)
  }
 
  def ResolveCouplingInvariant(ci: CouplingInvariant, cl: Class, context: ProgramContext) {
-- 
cgit v1.2.3