From 27f248f5e89ebc178e0be62ad1f73df58bc06786 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 19 Oct 2015 17:12:26 +0200
Subject: [PATCH] AnalysisPhase -> VerificationPhase
---
src/main/scala/leon/Main.scala | 10 +++++-----
.../leon/invariant/engine/InferInvariantsPhase.scala | 2 +-
src/main/scala/leon/repair/Repairman.scala | 4 ++--
src/main/scala/leon/synthesis/Synthesizer.scala | 2 +-
.../scala/leon/verification/VerificationContext.scala | 2 +-
.../{AnalysisPhase.scala => VerificationPhase.scala} | 6 +++---
.../scala/leon/regression/repair/RepairSuite.scala | 4 ++--
.../verification/LibraryVerificationSuite.scala | 4 ++--
.../leon/regression/verification/NewSolversSuite.scala | 2 +-
.../regression/verification/VerificationSuite.scala | 4 ++--
10 files changed, 20 insertions(+), 20 deletions(-)
rename src/main/scala/leon/verification/{AnalysisPhase.scala => VerificationPhase.scala} (96%)
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 3e8489948..45c62bd0d 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -21,7 +21,7 @@ object Main {
purescala.FunctionClosure,
synthesis.SynthesisPhase,
termination.TerminationPhase,
- verification.AnalysisPhase,
+ verification.VerificationPhase,
repair.RepairPhase,
evaluators.EvaluationPhase,
solvers.isabelle.AdaptationPhase,
@@ -147,7 +147,7 @@ object Main {
import synthesis.SynthesisPhase
import termination.TerminationPhase
import xlang.FixReportLabels
- import verification.AnalysisPhase
+ import verification.VerificationPhase
import repair.RepairPhase
import evaluators.EvaluationPhase
import solvers.isabelle.IsabellePhase
@@ -177,19 +177,19 @@ object Main {
ExtractionPhase andThen
new PreprocessingPhase(xlangF)
- val analysis = if (xlangF) AnalysisPhase andThen FixReportLabels else AnalysisPhase
+ val verification = if (xlangF) VerificationPhase andThen FixReportLabels else VerificationPhase
val pipeProcess: Pipeline[Program, Any] = {
if (noopF) RestoreMethods andThen FileOutputPhase
else if (synthesisF) SynthesisPhase
else if (repairF) RepairPhase
- else if (analysisF) Pipeline.both(analysis, TerminationPhase)
+ else if (analysisF) Pipeline.both(verification, TerminationPhase)
else if (terminationF) TerminationPhase
else if (isabelleF) IsabellePhase
else if (evalF) EvaluationPhase
else if (inferInvF) InferInvariantsPhase
else if (instrumentF) InstrumentationPhase andThen FileOutputPhase
- else analysis
+ else verification
}
pipeBegin andThen
diff --git a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
index ce69f2b6f..4bc1e245f 100644
--- a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
+++ b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
@@ -144,7 +144,7 @@ object InferInvariantsPhase extends SimpleLeonPhase[Program, InferenceReport] {
}
def validateAndCollectNotValidated(prog: Program, ctx: LeonContext, timeout: Int): Set[String] = {
- val verifyPipe = AnalysisPhase
+ val verifyPipe = VerificationPhase
val ctxWithTO = createLeonContext(ctx, "--timeout=" + timeout)
(verifyPipe.run(ctxWithTO, prog)._2).results.collect{
case (VC(_, fd, VCKinds.Postcondition), Some(vcRes)) if vcRes.isInconclusive =>
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index aac4a8d4a..1f939c96e 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -167,10 +167,10 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val timeoutMs = verifTimeoutMs.getOrElse(3000L)
val solverf = SolverFactory.getFromSettings(ctx, program).withTimeout(timeoutMs)
val vctx = VerificationContext(ctx, program, solverf, reporter)
- val vcs = AnalysisPhase.generateVCs(vctx, Seq(fd))
+ val vcs = VerificationPhase.generateVCs(vctx, Seq(fd))
try {
- val report = AnalysisPhase.checkVCs(
+ val report = VerificationPhase.checkVCs(
vctx,
vcs,
stopAfter = Some({ (vc, vr) => vr.isInvalid })
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 7ed4d56a8..54e305adf 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -70,7 +70,7 @@ class Synthesizer(val context : LeonContext,
}
def validateSolution(search: Search, sol: Solution, timeout: Duration): (Solution, Boolean) = {
- import verification.AnalysisPhase._
+ import verification.VerificationPhase._
import verification.VerificationContext
reporter.info("Solution requires validation")
diff --git a/src/main/scala/leon/verification/VerificationContext.scala b/src/main/scala/leon/verification/VerificationContext.scala
index ba3b5024e..2aaa910ab 100644
--- a/src/main/scala/leon/verification/VerificationContext.scala
+++ b/src/main/scala/leon/verification/VerificationContext.scala
@@ -12,5 +12,5 @@ case class VerificationContext (
solverFactory: SolverFactory[Solver],
reporter: Reporter
) {
- val checkInParallel: Boolean = context.findOptionOrDefault(AnalysisPhase.optParallelVCs)
+ val checkInParallel: Boolean = context.findOptionOrDefault(VerificationPhase.optParallelVCs)
}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/VerificationPhase.scala
similarity index 96%
rename from src/main/scala/leon/verification/AnalysisPhase.scala
rename to src/main/scala/leon/verification/VerificationPhase.scala
index e5edc1308..21119c4e2 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/VerificationPhase.scala
@@ -11,9 +11,9 @@ import java.lang.System
import solvers._
-object AnalysisPhase extends SimpleLeonPhase[Program,VerificationReport] {
- val name = "Analysis"
- val description = "Leon Verification"
+object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
+ val name = "Verification"
+ val description = "Verification of function contracts"
val optParallelVCs = LeonFlagOptionDef("parallel", "Check verification conditions in parallel", default = false)
diff --git a/src/test/scala/leon/regression/repair/RepairSuite.scala b/src/test/scala/leon/regression/repair/RepairSuite.scala
index 2ac93521b..50b845f92 100644
--- a/src/test/scala/leon/regression/repair/RepairSuite.scala
+++ b/src/test/scala/leon/regression/repair/RepairSuite.scala
@@ -7,7 +7,7 @@ import leon.test._
import leon.utils._
import leon.frontends.scalac.ExtractionPhase
import leon.repair._
-import leon.verification.AnalysisPhase
+import leon.verification.VerificationPhase
class RepairSuite extends LeonRegressionSuite {
val pipeline = ExtractionPhase andThen
@@ -35,7 +35,7 @@ class RepairSuite extends LeonRegressionSuite {
interruptManager = new InterruptManager(reporter),
options = Seq(
LeonOption(SharedOptions.optFunctions)(Seq(fileToFun(name))),
- LeonOption(AnalysisPhase.optParallelVCs)(true),
+ LeonOption(VerificationPhase.optParallelVCs)(true),
LeonOption(SharedOptions.optTimeout)(180L)
)
)
diff --git a/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala b/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
index bd4422698..d350bd04b 100644
--- a/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
@@ -6,13 +6,13 @@ import leon._
import leon.test._
import leon.frontends.scalac.ExtractionPhase
import leon.utils.PreprocessingPhase
-import leon.verification.AnalysisPhase
+import leon.verification.VerificationPhase
class LibraryVerificationSuite extends LeonRegressionSuite {
test("Verify the library") {
val pipeline = ExtractionPhase andThen
new PreprocessingPhase andThen
- AnalysisPhase
+ VerificationPhase
val ctx = Main.processOptions(Seq("--functions=_")).copy(reporter = new TestSilentReporter())
diff --git a/src/test/scala/leon/regression/verification/NewSolversSuite.scala b/src/test/scala/leon/regression/verification/NewSolversSuite.scala
index 6eac7183e..6065d8232 100644
--- a/src/test/scala/leon/regression/verification/NewSolversSuite.scala
+++ b/src/test/scala/leon/regression/verification/NewSolversSuite.scala
@@ -4,7 +4,7 @@ package leon.regression.verification
import _root_.smtlib.interpreters._
import leon._
-import leon.verification.AnalysisPhase
+import leon.verification.VerificationPhase
/* @EK: Disabled for now as many tests fail
class NewSolversSuite extends VerificationSuite {
diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala
index 06b00e0bb..b23fb0c4e 100644
--- a/src/test/scala/leon/regression/verification/VerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/VerificationSuite.scala
@@ -6,7 +6,7 @@ import leon._
import leon.test._
import leon.utils.UniqueCounter
-import leon.verification.{AnalysisPhase, VerificationReport}
+import leon.verification.{VerificationPhase, VerificationReport}
import leon.purescala.Definitions.Program
import leon.frontends.scalac.ExtractionPhase
import leon.utils.PreprocessingPhase
@@ -38,7 +38,7 @@ trait VerificationSuite extends LeonRegressionSuite {
val analysis =
(if (isabelle) AdaptationPhase else NoopPhase[Program]) andThen
- AnalysisPhase andThen
+ VerificationPhase andThen
(if (desugarXLang) FixReportLabels else NoopPhase[VerificationReport])
val ctx = createLeonContext(files:_*)
--
GitLab