From 6433777bd97e4e5b72d111957a2be30e4d9c7f02 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 18 Apr 2012 13:33:43 +0200
Subject: [PATCH] moving the application of pass from Analysis to Main
---
src/main/scala/leon/Analysis.scala | 6 +-----
src/main/scala/leon/DefaultTactic.scala | 2 --
src/main/scala/leon/Main.scala | 4 +++-
3 files changed, 4 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/Analysis.scala
index 546f27acf..6458079be 100644
--- a/src/main/scala/leon/Analysis.scala
+++ b/src/main/scala/leon/Analysis.scala
@@ -7,13 +7,9 @@ import purescala.TypeTrees._
import Extensions._
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)
- 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 trivialSolver = new TrivialSolver(reporter) // This one you can't disable :D
diff --git a/src/main/scala/leon/DefaultTactic.scala b/src/main/scala/leon/DefaultTactic.scala
index afba6d6f6..a01d02543 100644
--- a/src/main/scala/leon/DefaultTactic.scala
+++ b/src/main/scala/leon/DefaultTactic.scala
@@ -78,8 +78,6 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
expr2
}
}
- println("generating post condtion with: " + functionDefinition.fromLoop)
- println("for" + functionDefinition)
if(functionDefinition.fromLoop)
Seq(new VerificationCondition(theExpr, functionDefinition.parent.get, VCKind.InvariantPost, this.asInstanceOf[DefaultTactic]).setPosInfo(functionDefinition))
else
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index aefcf528a..72623c96a 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -31,7 +31,9 @@ object Main {
}
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
}
--
GitLab