From 7d353945347d4f8d03fa54c36fe148704477556f Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 6 May 2015 17:39:23 +0200
Subject: [PATCH] generate vc for division by zero
---
src/main/scala/leon/verification/DefaultTactic.scala | 3 +++
src/main/scala/leon/verification/InjectAsserts.scala | 12 ++++++++++++
.../leon/verification/VerificationCondition.scala | 1 +
.../verification/purescala/invalid/BVDivision.scala | 11 +++++++++++
.../verification/purescala/invalid/Division.scala | 11 +++++++++++
.../verification/purescala/valid/BVDivision.scala | 11 +++++++++++
.../verification/purescala/valid/Division.scala | 11 +++++++++++
7 files changed, 60 insertions(+)
create mode 100644 src/test/resources/regression/verification/purescala/invalid/BVDivision.scala
create mode 100644 src/test/resources/regression/verification/purescala/invalid/Division.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/BVDivision.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/Division.scala
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 70d8091b2..415f4edaa 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -49,6 +49,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
case e @ Error(_, "Match is non-exhaustive") =>
(e, VCKinds.ExhaustiveMatch, BooleanLiteral(false))
+
case e @ Error(_, _) =>
(e, VCKinds.Assert, BooleanLiteral(false))
@@ -57,6 +58,8 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
VCKinds.MapUsage
} else if (err.startsWith("Array ")) {
VCKinds.ArrayUsage
+ } else if (err.startsWith("Division ")) {
+ VCKinds.DivisionByZero
} else {
VCKinds.Assert
}
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index 8d0645e9b..3e371b3bc 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -30,6 +30,18 @@ object InjectAsserts extends LeonPhase[Program, Program] {
Some(Assert(indexUpTo(i, ArrayLength(a)), Some("Array index out of range"), e).setPos(e))
case e @ MapGet(m,k) =>
Some(Assert(MapIsDefinedAt(m, k), Some("Map undefined at this index"), e).setPos(e))
+
+ case e @ Division(_, d) =>
+ Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+ Some("Division by zero"),
+ e
+ ).setPos(e))
+ case e @ BVDivision(_, d) =>
+ Some(Assert(Not(Equals(d, IntLiteral(0))),
+ Some("Division by zero"),
+ e
+ ).setPos(e))
+
case _ =>
None
})
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 46e255d9c..890a16d06 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -34,6 +34,7 @@ object VCKinds {
case object ExhaustiveMatch extends VCKind("match exhaustiveness", "match.")
case object MapUsage extends VCKind("map usage", "map use")
case object ArrayUsage extends VCKind("array usage", "arr. use")
+ case object DivisionByZero extends VCKind("division by zero", "div 0")
}
case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option[Long]) {
diff --git a/src/test/resources/regression/verification/purescala/invalid/BVDivision.scala b/src/test/resources/regression/verification/purescala/invalid/BVDivision.scala
new file mode 100644
index 000000000..a2572db84
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/BVDivision.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object BVDivision {
+
+ def divByZero(x: Int): Boolean = {
+ (x / 0 == 10)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/Division.scala b/src/test/resources/regression/verification/purescala/invalid/Division.scala
new file mode 100644
index 000000000..6b505a773
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/Division.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object Division {
+
+ def divByZero(x: BigInt): Boolean = {
+ (x / BigInt(0) == BigInt(10))
+ }
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/BVDivision.scala b/src/test/resources/regression/verification/purescala/valid/BVDivision.scala
new file mode 100644
index 000000000..2121f416e
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/BVDivision.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object BVDivision {
+
+ def noDivByZero(x: Int): Boolean = {
+ (x / 10 == 10)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/Division.scala b/src/test/resources/regression/verification/purescala/valid/Division.scala
new file mode 100644
index 000000000..49337b86d
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Division.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object Division {
+
+ def noDivByZero(x: BigInt): Boolean = {
+ (x / BigInt(10) == BigInt(10))
+ }
+
+}
--
GitLab