From a1f0bcda196d1a1a7ef6bc33a23b5a3cca3d94fa Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 6 May 2015 18:00:43 +0200
Subject: [PATCH] Precise description of preconditions
---
src/main/scala/leon/verification/DefaultTactic.scala | 2 +-
src/main/scala/leon/verification/InductionTactic.scala | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index dd1458776..70d8091b2 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -34,7 +34,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
val pre2 = replaceFromIDs((tfd.params.map(_.id) zip args).toMap, pre)
val vc = implies(and(precOrTrue(fd), path), pre2)
- VC(vc, fd, VCKinds.Precondition, this).setPos(fi)
+ VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fi"), this).setPos(fi)
}
case None =>
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index efd77f876..27facb188 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -77,7 +77,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
val vc = implies(and(CaseClassInstanceOf(cct, arg.toVariable), precOrTrue(fd), path), implies(andJoin(subCases), replace((tfd.params.map(_.toVariable) zip args).toMap, pre)))
- VC(vc, fd, VCKinds.Info(VCKinds.Precondition, "ind. on $arg / ${cct.classDef.id}"), this).setPos(fi)
+ VC(vc, fd, VCKinds.Info(VCKinds.Precondition, "call $fi, ind. on $arg / ${cct.classDef.id}"), this).setPos(fi)
}
}
--
GitLab