AntiAliasing: restore var binding in mapApplication

epfl-lara · Apr 22, 2024 · f75c49c · f75c49c
1 parent c4b33d1
commit f75c49c
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 2 deletions.
diff --git a/.larabot.conf b/.larabot.conf
@@ -1,6 +1,6 @@
 commands = [
     "sbt -batch -Dtestsuite-parallelism=5 test"
-    "sbt -batch -Dtestsuite-parallelism=3 -Dtestcase-parallelism=5 \"stainless-dotty / IntegrationTest / testOnly stainless.GhostRewriteSuite stainless.GenCSuite stainless.LibrarySuite stainless.verification.VerificationSuite stainless.verification.UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.FullImperativeSuite stainless.verification.StrictArithmeticSuite stainless.termination.TerminationSuite stainless.evaluators.EvaluatorComponentTest\""
+    "sbt -batch -Dtestsuite-parallelism=3 -Dtestcase-parallelism=5 \"stainless-dotty / IntegrationTest / testOnly stainless.DottyExtractionSuite stainless.GhostRewriteSuite stainless.GenCSuite stainless.LibrarySuite stainless.verification.VerificationSuite stainless.verification.UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.FullImperativeSuite stainless.verification.StrictArithmeticSuite stainless.termination.TerminationSuite stainless.evaluators.EvaluatorComponentTest\""
 ]
 
 nightly {

diff --git a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala
@@ -436,7 +436,14 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
             }
 
             val extractResults = Block(assgns, TupleSelect(freshRes.toVariable, 1))
-            Let(freshRes, nfi, extractResults)
+            // FIXME: This should be `Let` and not `LetVar`, however doing so will cause a crash in e.g. `MapAliasing1`
+            //  because `getAllTargetsDealiased` in the `Let` case will result in an invalid target due to
+            //  this function not supporting targets computation on function application *post-transformation*.
+            if (isMutableType(nfiType)) {
+              LetVar(freshRes, nfi, extractResults)
+            } else {
+              Let(freshRes, nfi, extractResults)
+            }
           } else {
             nfi
           }