From 727354805f3c33d17bff18b74fc688b631e85f41 Mon Sep 17 00:00:00 2001 From: Alex AUVOLAT Date: Sun, 1 Jun 2014 10:13:41 +0200 Subject: Assert j != 0 in bound_div i j --- abstract/intervals_domain.ml | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) (limited to 'abstract/intervals_domain.ml') 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) -> -- cgit v1.2.3