AnalysisPhase -> VerificationPhase

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

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 =>

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 })

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")

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)
 }

src/main/scala/leon/verification/AnalysisPhase.scala → 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)
 

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)
       )
     )

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())
 

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 {

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:_*)