From d27932a5225c9176c0d0fab2f9e2312b64dcd1c7 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 21 Aug 2015 11:46:58 +0200
Subject: [PATCH] Bring back match exhaustiveness checks
---
.../leon/verification/DefaultTactic.scala | 8 ++---
.../purescala/invalid/MatchExh.scala | 35 +++++++++++++++++++
.../purescala/valid/MatchExh.scala | 18 ++++++++++
3 files changed, 57 insertions(+), 4 deletions(-)
create mode 100644 src/regression/resources/regression/verification/purescala/invalid/MatchExh.scala
create mode 100644 src/regression/resources/regression/verification/purescala/valid/MatchExh.scala
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 2bcd2eb0b..bba6f4fa2 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -46,9 +46,9 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
fd.body match {
case Some(body) =>
val calls = collectWithPC {
- case e @ Error(_, "Match is non-exhaustive") =>
- (e, VCKinds.ExhaustiveMatch, BooleanLiteral(false))
+ case m @ MatchExpr(scrut, cases) =>
+ (m, VCKinds.ExhaustiveMatch, orJoin(cases map (matchCaseCondition(scrut, _))))
case e @ Error(_, _) =>
(e, VCKinds.Assert, BooleanLiteral(false))
@@ -77,8 +77,8 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
}(body)
calls.map {
- case ((e, kind, errorCond), path) =>
- val vc = implies(and(precOrTrue(fd), path), errorCond)
+ case ((e, kind, correctnessCond), path) =>
+ val vc = implies(and(precOrTrue(fd), path), correctnessCond)
VC(vc, fd, kind, this).setPos(e)
}
diff --git a/src/regression/resources/regression/verification/purescala/invalid/MatchExh.scala b/src/regression/resources/regression/verification/purescala/invalid/MatchExh.scala
new file mode 100644
index 000000000..0f7f7d736
--- /dev/null
+++ b/src/regression/resources/regression/verification/purescala/invalid/MatchExh.scala
@@ -0,0 +1,35 @@
+import leon.lang._
+import leon.collection._
+
+object MatchExh {
+
+ def exh1(i: Int) = i match {
+ case 1 => 2
+ case 0 => 2
+ case _ => 2
+ }
+
+ def exh2[A](l: List[A]) = l match {
+ case Nil() => 0
+ case Cons(a, Nil()) => 1
+ case Cons(a, _) => 2
+ }
+
+ def err1(i: Int) = i match {
+ case 1 => 2
+ case 0 => 42
+ }
+
+ def err2[A](l: List[A]) = l match {
+ case Nil() => 0
+ case Cons(a, Nil()) => 1
+ case Cons(a, Cons(b, _)) if a == b => 2
+ }
+
+ def err3(l: List[BigInt]) = l match {
+ case Nil() => 0
+ case Cons(BigInt(0), Nil()) => 0
+ case Cons(_, Cons(_, _)) => 1
+ }
+
+}
diff --git a/src/regression/resources/regression/verification/purescala/valid/MatchExh.scala b/src/regression/resources/regression/verification/purescala/valid/MatchExh.scala
new file mode 100644
index 000000000..77251bc8c
--- /dev/null
+++ b/src/regression/resources/regression/verification/purescala/valid/MatchExh.scala
@@ -0,0 +1,18 @@
+import leon.lang._
+import leon.collection._
+
+object MatchExh {
+
+ def exh1(i: Int) = i match {
+ case 1 => 2
+ case 0 => 2
+ case _ => 2
+ }
+
+ def exh2[A](l: List[A]) = l match {
+ case Nil() => 0
+ case Cons(a, Nil()) => 1
+ case Cons(a, _) => 2
+ }
+
+}
--
GitLab