diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 6e0a85e0f41643e0040c1af2d04b1f3aea30a67c..546f49ac77db015a329ba26d1daf432534d1929d 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -687,7 +687,7 @@ object TreeOps {
(realCond, newRhs)
}
- val bigIte = condsAndRhs.foldRight[Expr](Error("non-exhaustive match").copiedFrom(m))((p1, ex) => {
+ val bigIte = condsAndRhs.foldRight[Expr](Error("Match is non-exhaustive").copiedFrom(m))((p1, ex) => {
if(p1._1 == BooleanLiteral(true)) {
p1._2
} else {
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeTreeOps.scala
index fc737493788fe49f9390f8d2034de86c6fdd5083..41c4041cf23843e0a8689099cc3e19a186a7266c 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeTreeOps.scala
@@ -61,6 +61,7 @@ object TypeTreeOps {
(_: SetType, _: SetType) |
(_: MapType, _: MapType) |
(_: FunctionType, _: FunctionType) =>
+
val NAryType(ts1, _) = tpe
val NAryType(ts2, _) = stpe
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 7e03ccebaf9c947c4206b38613474d7f1803f75c..71a8b8203756a7a8af7c51981d845bba150d100d 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -21,7 +21,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
val res = id.freshen
val vc = Implies(precOrTrue(fd), Let(res, safe(body), replace(Map(id.toVariable -> res.toVariable), safe(post))))
- Seq(new VerificationCondition(vc, fd, VCKind.Postcondition, this).setPos(post))
+ Seq(new VerificationCondition(vc, fd, VCPostcondition, this).setPos(post))
case _ =>
Nil
}
@@ -39,7 +39,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
val pre2 = replaceFromIDs((tfd.params.map(_.id) zip args).toMap, safe(pre))
val vc = Implies(And(precOrTrue(fd), path), pre2)
- new VerificationCondition(vc, fd, VCKind.Precondition, this).setPos(fi)
+ new VerificationCondition(vc, fd, VCPrecondition, this).setPos(fi)
}
case None =>
@@ -51,17 +51,32 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
fd.body match {
case Some(body) =>
val calls = collectWithPC {
- case e @ Error(_) => (e, BooleanLiteral(false))
- case a @ Assert(cond, _, _) => (a, cond)
+ case e @ Error("Match is non-exhaustive") =>
+ (e, VCExhaustiveMatch, BooleanLiteral(false))
+
+ case e @ Error(_) =>
+ (e, VCAssert, BooleanLiteral(false))
+
+ case a @ Assert(cond, Some(err), _) =>
+ val kind = if (err.startsWith("Map ")) {
+ VCMapUsage
+ } else if (err.startsWith("Array ")) {
+ VCArrayUsage
+ } else {
+ VCAssert
+ }
+
+ (a, kind, cond)
+ case a @ Assert(cond, None, _) => (a, VCAssert, cond)
// Only triggered for inner ensurings, general postconditions are handled by generatePostconditions
- case a @ Ensuring(body, id, post) => (a, Let(id, body, post))
+ case a @ Ensuring(body, id, post) => (a, VCAssert, Let(id, body, post))
}(safe(body))
calls.map {
- case ((e, errorCond), path) =>
+ case ((e, kind, errorCond), path) =>
val vc = Implies(And(precOrTrue(fd), path), errorCond)
- new VerificationCondition(vc, fd, VCKind.Correctness, this).setPos(e)
+ new VerificationCondition(vc, fd, kind, this).setPos(e)
}
case None =>
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 73b0655bd1ab1c92432815c044c2ee8a63697e80..97804cb7675bb34f27b409de1846a72b59c5b106 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) {
val vc = Implies(And(CaseClassInstanceOf(cct, arg.toVariable), precOrTrue(fd)), Implies(And(subCases), Let(id, body, post)))
- new VerificationCondition(vc, fd, VCKind.Postcondition, this).setPos(fd)
+ new VerificationCondition(vc, fd, VCPostcondition, this).setPos(fd)
}
case (body, _, post) =>
@@ -77,7 +77,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
val vc = Implies(And(Seq(CaseClassInstanceOf(cct, arg.toVariable), precOrTrue(fd), path)), Implies(And(subCases), replace((tfd.params.map(_.toVariable) zip args).toMap, pre)))
- new VerificationCondition(vc, fd, VCKind.Precondition, this).setPos(fi)
+ new VerificationCondition(vc, fd, VCPrecondition, this).setPos(fi)
}
}
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index fc905630d039d8c651443a8c384ebddc3f0f98ad..3b2a9268dc4d838feaddd7e3cbf2e6086795c551 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -10,7 +10,7 @@ import leon.utils.{Position, Positioned}
import leon.solvers._
/** This is just to hold some history information. */
-class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: VCKind.Value, val tactic: Tactic, val info: String = "") extends Positioned {
+class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: VCKind, val tactic: Tactic, val info: String = "") extends Positioned {
// None = still unknown
// Some(true) = valid
// Some(false) = valid
@@ -37,15 +37,10 @@ class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: V
}
}
-object VCKind extends Enumeration {
- val Precondition = Value("precond.")
- val Postcondition = Value("postcond.")
- val Correctness = Value("correct.")
- val ExhaustiveMatch = Value("match.")
- val MapAccess = Value("map acc.")
- val ArrayAccess = Value("arr. acc.")
- val InvariantInit = Value("inv init.")
- val InvariantInd = Value("inv ind.")
- val InvariantPost = Value("inv post.")
- val InvariantPre = Value("inv pre.")
-}
+abstract class VCKind(val name: String, val abbrv: String)
+case object VCPrecondition extends VCKind("precondition", "precond.")
+case object VCPostcondition extends VCKind("postcondition", "postcond.")
+case object VCAssert extends VCKind("body assertion", "assert.")
+case object VCExhaustiveMatch extends VCKind("match exhaustivness", "match.")
+case object VCMapUsage extends VCKind("map usage", "map use")
+case object VCArrayUsage extends VCKind("array usage", "arr. use")
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index a504b478f0a7243f45e8359b790d9f3f6c2c0059..27e25e6613362c4d3106278b36c5bb7c416fab82 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -28,7 +28,7 @@ class VerificationReport(val fvcs: Map[FunDef, List[VerificationCondition]]) {
val timeStr = vc.time.map(t => "%-3.3f".format(t)).getOrElse("")
Row(Seq(
Cell(vc.funDef.id.toString),
- Cell(vc.kind),
+ Cell(vc.kind.name),
Cell(vc.status),
Cell(vc.tacticStr),
Cell(vc.solverStr),
diff --git a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
index ad1c5e61511bc9712cc453e1adbf13eb8da082d3..3d236b1b4810570fc11e494722a71c025f8633d3 100644
--- a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
@@ -11,6 +11,9 @@ object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
val name = "xlang analysis"
val description = "apply analysis on xlang"
+ case object VCInvariantPost extends VCKind("invariant postcondition", "inv. post.")
+ case object VCInvariantInd extends VCKind("invariant inductive", "inv. ind.")
+
def run(ctx: LeonContext)(pgm: Program): VerificationReport = {
val pgm1 = ArrayTransformation(ctx, pgm)
@@ -70,7 +73,7 @@ object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
val freshVc = new VerificationCondition(
vc.condition,
funDef.parent.getOrElse(funDef),
- if(vc.kind == VCKind.Postcondition) VCKind.InvariantPost else if(vc.kind == VCKind.Precondition) VCKind.InvariantInd else vc.kind,
+ if(vc.kind == VCPostcondition) VCInvariantPost else if(vc.kind == VCPrecondition) VCInvariantInd else vc.kind,
vc.tactic,
vc.info).setPos(funDef)
freshVc.value = vc.value