From 031954edfddf92f4f73ed62453311cbb834a8837 Mon Sep 17 00:00:00 2001
From: Lars Hupel <lars.hupel@mytum.de>
Date: Wed, 2 Sep 2015 18:14:29 +0200
Subject: [PATCH] don't store the tactic in the VC
---
src/main/scala/leon/verification/DefaultTactic.scala | 6 +++---
src/main/scala/leon/verification/InductionTactic.scala | 4 ++--
.../scala/leon/verification/VerificationCondition.scala | 2 +-
src/main/scala/leon/xlang/FixReportLabels.scala | 3 +--
4 files changed, 7 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index bba6f4fa2..616f3420d 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -16,7 +16,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
case (Some(post), Some(body)) =>
val vc = implies(precOrTrue(fd), application(post, Seq(body)))
- Seq(VC(vc, fd, VCKinds.Postcondition, this).setPos(post))
+ Seq(VC(vc, fd, VCKinds.Postcondition).setPos(post))
case _ =>
Nil
}
@@ -34,7 +34,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
val pre2 = tfd.withParamSubst(args, pre)
val vc = implies(and(precOrTrue(fd), path), pre2)
val fiS = sizeLimit(fi.asString, 40)
- VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS"), this).setPos(fi)
+ VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS")).setPos(fi)
}
case None =>
@@ -80,7 +80,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
case ((e, kind, correctnessCond), path) =>
val vc = implies(and(precOrTrue(fd), path), correctnessCond)
- VC(vc, fd, kind, this).setPos(e)
+ VC(vc, fd, kind).setPos(e)
}
case None =>
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 878b902ce..9e06e4abd 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -44,7 +44,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
implies(andJoin(subCases), application(post, Seq(body)))
)
- VC(vc, fd, VCKinds.Info(VCKinds.Postcondition, s"ind. on ${arg.asString} / ${cct.classDef.id.asString}"), this).setPos(fd)
+ VC(vc, fd, VCKinds.Info(VCKinds.Postcondition, s"ind. on ${arg.asString} / ${cct.classDef.id.asString}")).setPos(fd)
}
case (body, _, post) =>
@@ -84,7 +84,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
// Crop the call to display it properly
val fiS = sizeLimit(fi.asString, 25)
- VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS, ind. on (${arg.asString} : ${cct.classDef.id.asString})"), this).setPos(fi)
+ VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS, ind. on (${arg.asString} : ${cct.classDef.id.asString})")).setPos(fi)
}
case (body, _) =>
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index ba23961e3..8ddbf97ab 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -11,7 +11,7 @@ import leon.utils.Positioned
import leon.solvers._
/** This is just to hold some history information. */
-case class VC(condition: Expr, fd: FunDef, kind: VCKind, tactic: Tactic) extends Positioned {
+case class VC(condition: Expr, fd: FunDef, kind: VCKind) extends Positioned {
override def toString = {
fd.id.name +" - " +kind.toString
}
diff --git a/src/main/scala/leon/xlang/FixReportLabels.scala b/src/main/scala/leon/xlang/FixReportLabels.scala
index 91eabf9c3..614057b3b 100644
--- a/src/main/scala/leon/xlang/FixReportLabels.scala
+++ b/src/main/scala/leon/xlang/FixReportLabels.scala
@@ -36,8 +36,7 @@ object FixReportLabels extends LeonPhase[VerificationReport, VerificationReport]
val nvc = VC(
vc.condition,
fd,
- vcKind,
- vc.tactic
+ vcKind
).setPos(vc.getPos)
nvc -> ovr
--
GitLab