From d9b9c41dfaca41a4f0a354365c3d102e6441e56c Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <samuel.gruetter@epfl.ch>
Date: Tue, 2 Jun 2015 13:12:30 +0200
Subject: [PATCH] --verify --termination does verification and termination
checking in one run
---
src/main/scala/leon/Main.scala | 6 ++++++
src/main/scala/leon/Pipeline.scala | 13 +++++++++++++
2 files changed, 19 insertions(+)
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 66a54ec4c..04df65e6d 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -149,6 +149,7 @@ object Main {
val synthesisF = ctx.findOptionOrDefault(optSynthesis)
val xlangF = ctx.findOptionOrDefault(optXLang)
val repairF = ctx.findOptionOrDefault(optRepair)
+ val analysisF = ctx.findOption(optVerify).isDefined && ctx.findOption(optTermination).isDefined
val terminationF = ctx.findOptionOrDefault(optTermination)
val verifyF = ctx.findOptionOrDefault(optVerify)
val evalF = ctx.findOption(SharedOptions.optEval)
@@ -182,6 +183,7 @@ object Main {
if (noopF) RestoreMethods andThen FileOutputPhase
else if (synthesisF) SynthesisPhase
else if (repairF) RepairPhase
+ else if (analysisF) Pipeline.both(FunctionClosure andThen AnalysisPhase, TerminationPhase)
else if (terminationF) TerminationPhase
else if (xlangF) XLangAnalysisPhase
else if (evalF.isDefined) EvaluationPhase
@@ -246,6 +248,10 @@ object Main {
// Run pipeline
pipeline.run(ctx)(args.toList) match {
+ case (vReport: verification.VerificationReport, tReport: termination.TerminationReport) =>
+ ctx.reporter.info(vReport.summaryString)
+ ctx.reporter.info(tReport.summaryString)
+
case report: verification.VerificationReport =>
ctx.reporter.info(report.summaryString)
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index e4f93fcfa..3e3c8a915 100644
--- a/src/main/scala/leon/Pipeline.scala
+++ b/src/main/scala/leon/Pipeline.scala
@@ -15,3 +15,16 @@ abstract class Pipeline[-F, +T] {
def run(ctx: LeonContext)(v: F): T
}
+
+object Pipeline {
+
+ def both[T, R1, R2](f1: Pipeline[T, R1], f2: Pipeline[T, R2]): Pipeline[T, (R1, R2)] = new Pipeline[T, (R1, R2)] {
+ def run(ctx : LeonContext)(t : T): (R1, R2) = {
+ val r1 = f1.run(ctx)(t)
+ // don't check for SharedOptions.optStrictPhases because f2 does not depend on the result of f1
+ val r2 = f2.run(ctx)(t)
+ (r1, r2)
+ }
+ }
+
+}
--
GitLab