summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex AUVOLAT <alex.auvolat@ens.fr>2014-06-01 10:13:41 +0200
committerAlex AUVOLAT <alex.auvolat@ens.fr>2014-06-01 10:13:41 +0200
commit727354805f3c33d17bff18b74fc688b631e85f41 (patch)
treea6c5eb95d93fb045d8c0795d9c8d213252cab4b6
parent652d04c5476fdfb9cc7a2d93de3df4d76a6882ce (diff)
downloadSemVerif-Projet-727354805f3c33d17bff18b74fc688b631e85f41.tar.gz
SemVerif-Projet-727354805f3c33d17bff18b74fc688b631e85f41.zip
Assert j != 0 in bound_div i j
-rw-r--r--abstract/intervals_domain.ml9
1 files changed, 2 insertions, 7 deletions
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml
index d95a938..06c5e57 100644
--- a/abstract/intervals_domain.ml
+++ b/abstract/intervals_domain.ml
@@ -43,10 +43,8 @@ module Intervals : VALUE_DOMAIN = struct
if i < Z.zero then PInf
else MInf
| Int i, Int j ->
- if j = Z.zero then
- if i < Z.zero then MInf
- else PInf
- else Int (Z.div i j)
+ assert (j != Z.zero);
+ Int (Z.div i j)
let bound_min a b = match a, b with
@@ -116,8 +114,6 @@ module Intervals : VALUE_DOMAIN = struct
(bound_min (bound_mul b c) (bound_mul b d))),
(bound_max (bound_max (bound_mul a c) (bound_mul a d))
(bound_max (bound_mul b c) (bound_mul b d))))
-
-
let div a b = match a, b with
| Bot, _ -> Bot
| Itv(a, b), q ->
@@ -132,7 +128,6 @@ module Intervals : VALUE_DOMAIN = struct
Itv(min (bound_div b c) (bound_div b d), max (bound_div a c) (bound_div a d))
in
join p1 p2
-
let rem a b = match a, b with
| Bot, _ | _, Bot -> Bot
| Itv(a, b), Itv(c, d) ->