diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 7b6ccdcd60b89ac8d3351ff10159da689edd85e3..bbee52fbfe443e1284b45de9f6ef0f56f4f700f7 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -625,11 +625,11 @@ class PrettyPrinter(opts: PrinterOptions,
def precedence(ex: Expr): Int = ex match {
case (pa: PrettyPrintable) => pa.printPrecedence
case (_: ElementOfSet) => 0
- case (_: Or | BinaryMethodCall(_, "||", _)) => 1
+ case (_: Modulo) => 1
+ case (_: Or | BinaryMethodCall(_, "||", _)) => 2
case (_: And | BinaryMethodCall(_, "&&", _)) => 3
case (_: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan) => 4
case (_: Equals | _: Not) => 5
- case (_: Modulo) => 6
case (_: Plus | _: BVPlus | _: Minus | _: BVMinus | _: SetUnion| _: SetDifference | BinaryMethodCall(_, "+" | "-", _)) => 7
case (_: Times | _: BVTimes | _: Division | _: BVDivision | _: Remainder | _: BVRemainder | BinaryMethodCall(_, "*" | "/", _)) => 8
case _ => 9
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 2333c319170b5cd401d3dd177dd3104f78606a9b..43ef19dfdf281654b9288d589c3805586ed03e6a 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -60,6 +60,10 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
VCKinds.ArrayUsage
} else if (err.startsWith("Division ")) {
VCKinds.DivisionByZero
+ } else if (err.startsWith("Modulo ")) {
+ VCKinds.ModuloByZero
+ } else if (err.startsWith("Remainder ")) {
+ VCKinds.RemainderByZero
} else {
VCKinds.Assert
}
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index bacfbe1406df7ebaf1ecfe5772e18e1812a397be..fae6329c855c29d29fdc99cd8e300f19f2d21c14 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -13,7 +13,7 @@ import xlang.Expressions._
object InjectAsserts extends LeonPhase[Program, Program] {
val name = "Asserts"
- val description = "Inject asserts for various corrected conditions (map accesses, array accesses, ..)"
+ val description = "Inject asserts for various correctness conditions (map accesses, array accesses, divisions by zero,..)"
def run(ctx: LeonContext)(pgm: Program): Program = {
def indexUpTo(i: Expr, e: Expr) = {
@@ -40,11 +40,27 @@ object InjectAsserts extends LeonPhase[Program, Program] {
Some("Division by zero"),
e
).setPos(e))
+ case e @ Remainder(_, d) =>
+ Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+ Some("Remainder by zero"),
+ e
+ ).setPos(e))
+ case e @ Modulo(_, d) =>
+ Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+ Some("Modulo by zero"),
+ e
+ ).setPos(e))
+
case e @ BVDivision(_, d) =>
Some(Assert(Not(Equals(d, IntLiteral(0))),
Some("Division by zero"),
e
).setPos(e))
+ case e @ BVRemainder(_, d) =>
+ Some(Assert(Not(Equals(d, IntLiteral(0))),
+ Some("Remainder 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 890a16d065c7a142aa3aae5e67aaab4cace46faa..2063902c2bd290e03e08966471376a4c11794d2f 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -35,6 +35,8 @@ object VCKinds {
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 object ModuloByZero extends VCKind("modulo by zero", "mod 0")
+ case object RemainderByZero extends VCKind("remainder by zero", "rem 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/BVDivisionByZero.scala
similarity index 82%
rename from src/test/resources/regression/verification/purescala/invalid/BVDivision.scala
rename to src/test/resources/regression/verification/purescala/invalid/BVDivisionByZero.scala
index a2572db84870fa38ab5f4f6a924ddbaa1641d47f..54ac21fb62450e2f018a33c3e80be95edd8578c8 100644
--- a/src/test/resources/regression/verification/purescala/invalid/BVDivision.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/BVDivisionByZero.scala
@@ -2,7 +2,7 @@ import leon.lang._
import leon.collection._
import leon._
-object BVDivision {
+object BVDivisionByZero {
def divByZero(x: Int): Boolean = {
(x / 0 == 10)
diff --git a/src/test/resources/regression/verification/purescala/invalid/BVRemainderByZero.scala b/src/test/resources/regression/verification/purescala/invalid/BVRemainderByZero.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ed3ebf22a15764a06c65e3e55c219467987dc52a
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/BVRemainderByZero.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object BVRemainderByZero {
+
+ def remByZero(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/DivisionByZero.scala
similarity index 84%
rename from src/test/resources/regression/verification/purescala/invalid/Division.scala
rename to src/test/resources/regression/verification/purescala/invalid/DivisionByZero.scala
index 6b505a7732f6a6b0126e2c4b4106c16426069823..7415f2e6a8b1f0e9bded4fa90937f54bd0e0d5ea 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Division.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/DivisionByZero.scala
@@ -2,10 +2,10 @@ import leon.lang._
import leon.collection._
import leon._
-object Division {
+object DivisionByZero {
def divByZero(x: BigInt): Boolean = {
(x / BigInt(0) == BigInt(10))
}
-
+
}
diff --git a/src/test/resources/regression/verification/purescala/invalid/ModuloByZero.scala b/src/test/resources/regression/verification/purescala/invalid/ModuloByZero.scala
new file mode 100644
index 0000000000000000000000000000000000000000..19eb0da32576052ae96ac66408b74e8cfb9b2563
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/ModuloByZero.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object ModuloByZero {
+
+ def modByZero(x: BigInt): Boolean = {
+ (x mod BigInt(0)) == BigInt(10)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/RemainderByZero.scala b/src/test/resources/regression/verification/purescala/invalid/RemainderByZero.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5fc587fe8cfdfeca00a1ffebf311059eb971eedd
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/RemainderByZero.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object RemainderByZero {
+
+ def remByZero(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/BVDivisionByZero.scala
similarity index 57%
rename from src/test/resources/regression/verification/purescala/valid/BVDivision.scala
rename to src/test/resources/regression/verification/purescala/valid/BVDivisionByZero.scala
index 2121f416e3fe776c50f0502c6439c55832ad0cc0..3de75f00349da0b93c61a33c3b38f9c252d60149 100644
--- a/src/test/resources/regression/verification/purescala/valid/BVDivision.scala
+++ b/src/test/resources/regression/verification/purescala/valid/BVDivisionByZero.scala
@@ -2,10 +2,14 @@ import leon.lang._
import leon.collection._
import leon._
-object BVDivision {
+object BVDivisionByZero {
def noDivByZero(x: Int): Boolean = {
(x / 10 == 10)
}
+
+ def noRemByZero(x: BigInt): Boolean = {
+ (x % 10 == 10)
+ }
}
diff --git a/src/test/resources/regression/verification/purescala/valid/BVDivision2.scala b/src/test/resources/regression/verification/purescala/valid/BVDivisionByZero2.scala
similarity index 83%
rename from src/test/resources/regression/verification/purescala/valid/BVDivision2.scala
rename to src/test/resources/regression/verification/purescala/valid/BVDivisionByZero2.scala
index 77d677753e0c8aed018625f14d3d3b6d0a5ee0e8..382dbb1918d35f401af3c61d5d703e2a920cf2d6 100644
--- a/src/test/resources/regression/verification/purescala/valid/BVDivision2.scala
+++ b/src/test/resources/regression/verification/purescala/valid/BVDivisionByZero2.scala
@@ -2,7 +2,7 @@ import leon.lang._
import leon.collection._
import leon._
-object BVDivision2 {
+object BVDivisionByZero2 {
def division(x: Int, y: Int): Int = {
require(y != 0)
diff --git a/src/test/resources/regression/verification/purescala/valid/Division.scala b/src/test/resources/regression/verification/purescala/valid/Division.scala
deleted file mode 100644
index 49337b86d39a4a0199999d9380ef49c9d56fd569..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/verification/purescala/valid/Division.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-import leon.lang._
-import leon.collection._
-import leon._
-
-object Division {
-
- def noDivByZero(x: BigInt): Boolean = {
- (x / BigInt(10) == BigInt(10))
- }
-
-}
diff --git a/src/test/resources/regression/verification/purescala/valid/DivisionByZero.scala b/src/test/resources/regression/verification/purescala/valid/DivisionByZero.scala
new file mode 100644
index 0000000000000000000000000000000000000000..559e13591a0b52bbee82ae42d1b5e37cfbe79a88
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/DivisionByZero.scala
@@ -0,0 +1,19 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object DivisionByZero {
+
+ def noDivByZero(x: BigInt): Boolean = {
+ (x / BigInt(10) == BigInt(10))
+ }
+
+ def noRemByZero(x: BigInt): Boolean = {
+ (x % BigInt(10) == BigInt(10))
+ }
+
+ def noModByZero(x: BigInt): Boolean = {
+ (x mod BigInt(10)) == BigInt(10)
+ }
+
+}