Chalice: Fix two nasty bugs that could lead to contradictions in the Boogie encoding for certain programs. See workitems 10203 and 10204.

1 files changed, 4 insertions, 1 deletions

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index f6fea537..af9fc81b 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -346,7 +346,9 @@ case class Release(obj: Expression) extends Statement
 case class RdAcquire(obj: Expression) extends Statement

 case class RdRelease(obj: Expression) extends Statement

 case class Downgrade(obj: Expression) extends Statement

-case class Lock(obj: Expression, b: BlockStmt, rdLock: Boolean) extends Statement

+case class Lock(obj: Expression, b: BlockStmt, rdLock: Boolean) extends Statement {

+  override def Targets = b.Targets

+}

 case class Free(obj: Expression) extends Statement

 case class CallAsync(declaresLocal: Boolean, lhs: VariableExpr, obj: Expression, id: String, args: List[Expression]) extends Statement {

   var local: Variable = null

@@ -368,6 +370,7 @@ case class Send(ch: Expression, args: List[Expression]) extends Statement {
 case class Receive(declaresLocal: List[Boolean], ch: Expression, outs: List[VariableExpr]) extends Statement {

   var locals = List[Variable]()

   override def Declares = locals

+  override def Targets = (outs :\ Set[Variable]()) { (ve, vars) => if (ve.v != null) vars + ve.v else vars }

 }

 case class Fold(pred: Access) extends Statement

 case class Unfold(pred: Access) extends Statement