Fixed scoping of let in PureMethodsToFunctions

utwente-fmt · Nov 28, 2024 · ce2783c · ce2783c
1 parent f7b0f0c
commit ce2783c
Showing 1 changed file with 16 additions and 15 deletions.
diff --git a/src/rewrite/vct/rewrite/PureMethodsToFunctions.scala b/src/rewrite/vct/rewrite/PureMethodsToFunctions.scala
@@ -33,9 +33,6 @@ case class PureMethodsToFunctions[Pre <: Generation]() extends Rewriter[Pre] {
 
   val currentAbstractMethod: ScopedStack[AbstractMethod[Pre]] = ScopedStack()
 
-  private val variableMap: SuccessionMap[Variable[Pre], Variable[Post]] =
-    SuccessionMap()
-
   def countAssignments(v: Variable[Pre], s: Statement[Pre]): Option[Int] =
     s match {
       case Return(_) => Some(0)
@@ -98,18 +95,22 @@ case class PureMethodsToFunctions[Pre <: Generation]() extends Rewriter[Pre] {
         }
         toExpression(impl, alt)
       case Assign(Local(ref), e) =>
-        alt match {
-          case Some(exprAlt) =>
-            val vDecl = variableMap.getOrElseUpdate(
-              ref.decl,
-              variables.collect { dispatch(ref.decl) }._1.head,
-            )
-            Some(Let[Post](vDecl, dispatch(e), exprAlt))
-          case None =>
-            throw MethodCannotIntoFunction(
-              currentAbstractMethod.top,
-              "Pure method cannot end with assign statement",
-            )
+        localHeapVariables.scope {
+          variables.scope {
+            alt match {
+              case Some(exprAlt) =>
+                Some(Let[Post](
+                  variables.collect { dispatch(ref.decl) }._1.head,
+                  dispatch(e),
+                  exprAlt,
+                ))
+              case None =>
+                throw MethodCannotIntoFunction(
+                  currentAbstractMethod.top,
+                  "Pure method cannot end with assign statement",
+                )
+            }
+          }
         }
 
       case _ => None