From 0b232f11d50f7c93bb77f4df77b904721ed0d384 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 17 Jul 2015 17:37:54 +0200
Subject: [PATCH] check for division by zero of real numbers
---
src/main/scala/leon/verification/InjectAsserts.scala | 6 ++++++
.../purescala/invalid/RealDivisionByZero.scala | 11 +++++++++++
.../purescala/valid/RealDivisionByZero.scala | 11 +++++++++++
3 files changed, 28 insertions(+)
create mode 100644 src/test/resources/regression/verification/purescala/invalid/RealDivisionByZero.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/RealDivisionByZero.scala
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index fae6329c8..2710b3994 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -62,6 +62,12 @@ object InjectAsserts extends LeonPhase[Program, Program] {
e
).setPos(e))
+ case e @ RealDivision(_, d) =>
+ Some(Assert(Not(Equals(d, RealLiteral(0))),
+ Some("Division by zero"),
+ e
+ ).setPos(e))
+
case _ =>
None
})
diff --git a/src/test/resources/regression/verification/purescala/invalid/RealDivisionByZero.scala b/src/test/resources/regression/verification/purescala/invalid/RealDivisionByZero.scala
new file mode 100644
index 000000000..418fbb9e8
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/RealDivisionByZero.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object RealDivisionByZero {
+
+ def divByZero(x: Real): Boolean = {
+ (x / Real(0) == Real(10))
+ }
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/RealDivisionByZero.scala b/src/test/resources/regression/verification/purescala/valid/RealDivisionByZero.scala
new file mode 100644
index 000000000..3d8dcf5b2
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/RealDivisionByZero.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object RealDivisionByZero {
+
+ def noDivByZero(x: Real): Boolean = {
+ (x / Real(10) == Real(10))
+ }
+
+}
--
GitLab