From d0ff6838d8bdf8a982e0eb22b12e8b1ccec07ad9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Thu, 28 Apr 2016 17:32:04 +0200
Subject: [PATCH] Better exception mechanism for Input coverage.
---
.../leon/synthesis/disambiguation/InputCoverage.scala | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala b/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
index f1cdfd2b4..cdf471836 100644
--- a/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
@@ -27,6 +27,8 @@ import leon.verification.VCStatus
import leon.verification.VCResult
import leon.evaluators.AbstractEvaluator
+case class InputNotCoveredException(msg: String, lineExpr: Identifier) extends Exception(msg)
+
/**
* @author Mikael
* If possible, synthesizes a set of inputs for the function so that they cover all parts of the function.
@@ -43,10 +45,10 @@ class InputCoverage(fd: FunDef, fds: Set[FunDef])(implicit c: LeonContext, p: Pr
Else it creates a new boolean indicating this branch. */
def wrapBranch(e: (Expr, Option[Seq[Identifier]])): (Expr, Some[Seq[Identifier]]) = e._2 match {
case None =>
- val b = FreshIdentifier("l" + Math.abs(e._1.getPos.line) + "c" + Math.abs(e._1.getPos.col), BooleanType)
+ val b = FreshIdentifier("l" + Math.abs(e._1.getPos.line) + "c" + Math.abs(e._1.getPos.col), BooleanType).copiedFrom(e._1)
(tupleWrap(Seq(e._1, Variable(b))), Some(Seq(b)))
case Some(Seq()) =>
- val b = FreshIdentifier("l" + Math.abs(e._1.getPos.line) + "c" + Math.abs(e._1.getPos.col), BooleanType)
+ val b = FreshIdentifier("l" + Math.abs(e._1.getPos.line) + "c" + Math.abs(e._1.getPos.col), BooleanType).copiedFrom(e._1)
def putInLastBody(e: Expr): Expr = e match {
case Tuple(Seq(v, prev_b)) => Tuple(Seq(v, or(prev_b, b.toVariable))).copiedFrom(e)
@@ -262,7 +264,8 @@ class InputCoverage(fd: FunDef, fds: Set[FunDef])(implicit c: LeonContext, p: Pr
Set(bvar)
}
finalExprs -> coveredBooleansForCE
- case _ => Seq() -> Set(bvar)
+ case e =>
+ throw InputNotCoveredException("Could not find an input to cover the line: " + bvar.getPos.line + " (at col " + bvar.getPos.col + ")\n" + e.getOrElse(""), bvar)
}
}
--
GitLab