Skip to content
Snippets Groups Projects
Commit 6433777b authored by Régis Blanc's avatar Régis Blanc
Browse files

moving the application of pass from Analysis to Main

parent 11e503aa
Branches
Tags
No related merge requests found
...@@ -7,13 +7,9 @@ import purescala.TypeTrees._ ...@@ -7,13 +7,9 @@ import purescala.TypeTrees._
import Extensions._ import Extensions._
import scala.collection.mutable.{Set => MutableSet} import scala.collection.mutable.{Set => MutableSet}
class Analysis(pgm : Program, val reporter: Reporter = Settings.reporter) { class Analysis(val program : Program, val reporter: Reporter = Settings.reporter) {
Extensions.loadAll(reporter) Extensions.loadAll(reporter)
println("Analysis on program:\n" + pgm)
val passManager = new PassManager(Seq(ImperativeCodeElimination, UnitElimination, FunctionClosure, FunctionHoisting, Simplificator))
val program = passManager.run(pgm)
val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions
val trivialSolver = new TrivialSolver(reporter) // This one you can't disable :D val trivialSolver = new TrivialSolver(reporter) // This one you can't disable :D
......
...@@ -78,8 +78,6 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) { ...@@ -78,8 +78,6 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
expr2 expr2
} }
} }
println("generating post condtion with: " + functionDefinition.fromLoop)
println("for" + functionDefinition)
if(functionDefinition.fromLoop) if(functionDefinition.fromLoop)
Seq(new VerificationCondition(theExpr, functionDefinition.parent.get, VCKind.InvariantPost, this.asInstanceOf[DefaultTactic]).setPosInfo(functionDefinition)) Seq(new VerificationCondition(theExpr, functionDefinition.parent.get, VCKind.InvariantPost, this.asInstanceOf[DefaultTactic]).setPosInfo(functionDefinition))
else else
......
...@@ -31,7 +31,9 @@ object Main { ...@@ -31,7 +31,9 @@ object Main {
} }
private def defaultAction(program: Program, reporter: Reporter) : Unit = { private def defaultAction(program: Program, reporter: Reporter) : Unit = {
val analysis = new Analysis(program, reporter) val passManager = new PassManager(Seq(ImperativeCodeElimination, UnitElimination, FunctionClosure, FunctionHoisting, Simplificator))
val program2 = passManager.run(program)
val analysis = new Analysis(program2, reporter)
analysis.analyse analysis.analyse
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment