From b3559b983b9779b5241ccc2911f4eaf12bdc87f0 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 11 Sep 2015 16:07:01 +0200
Subject: [PATCH] Mutable field in an object? I don't think so.
This is a dirty quick fix for now until we rewrite the FunctionClosure
phase.
---
src/main/scala/leon/Main.scala | 6 +++---
src/main/scala/leon/purescala/FunctionClosure.scala | 3 +--
src/main/scala/leon/xlang/XLangDesugaringPhase.scala | 2 +-
.../leon/regression/synthesis/StablePrintingSuite.scala | 2 +-
4 files changed, 6 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 5ba9bfa53..8be3134c7 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -17,7 +17,7 @@ object Main {
xlang.ImperativeCodeElimination,
xlang.FixReportLabels,
xlang.XLangDesugaringPhase,
- purescala.FunctionClosure,
+ new purescala.FunctionClosure,
synthesis.SynthesisPhase,
termination.TerminationPhase,
verification.AnalysisPhase,
@@ -190,12 +190,12 @@ object Main {
else if (synthesisF) SynthesisPhase
else if (repairF) RepairPhase
else if (analysisF) Pipeline.both(
- FunctionClosure andThen analysis,
+ (new FunctionClosure) andThen analysis,
TerminationPhase
)
else if (terminationF) TerminationPhase
else if (evalF) EvaluationPhase
- else FunctionClosure andThen analysis
+ else (new FunctionClosure) andThen analysis
}
pipeBegin andThen
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 96ef8e2b0..4ac11044d 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -10,7 +10,7 @@ import Extractors._
import ExprOps._
import Constructors._
-object FunctionClosure extends TransformationPhase {
+class FunctionClosure extends TransformationPhase {
val name = "Function Closure"
val description = "Closing function with its scoping variables"
@@ -175,5 +175,4 @@ object FunctionClosure extends TransformationPhase {
} while(newVars != Set())
(filteredConstraints, allVars)
}
-
}
diff --git a/src/main/scala/leon/xlang/XLangDesugaringPhase.scala b/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
index f891b212e..6b06991c7 100644
--- a/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
+++ b/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
@@ -16,7 +16,7 @@ object XLangDesugaringPhase extends TransformationPhase {
ArrayTransformation andThen
EpsilonElimination andThen
ImperativeCodeElimination andThen
- FunctionClosure
+ (new FunctionClosure)
phases.run(ctx)(pgm)
}
diff --git a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
index 99f8bcfa8..9cd16293f 100644
--- a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
@@ -33,7 +33,7 @@ class StablePrintingSuite extends LeonRegressionSuite {
val pipeline = leon.utils.TemporaryInputPhase andThen
frontends.scalac.ExtractionPhase andThen
leon.utils.PreprocessingPhase andThen
- purescala.FunctionClosure
+ (new purescala.FunctionClosure)
val program = pipeline.run(ctx)((List(content), Nil))
--
GitLab