diff options
Diffstat (limited to 'abstract/intervals_domain.ml')
| -rw-r--r-- | abstract/intervals_domain.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml index 92d00a2..084e397 100644 --- a/abstract/intervals_domain.ml +++ b/abstract/intervals_domain.ml @@ -10,6 +10,8 @@ module VD : VALUE_DOMAIN = struct | Int a, Int b -> a <= b | x, y -> x = y + let bound_lt a b = not (bound_leq b a) (* a < b *) + let bound_add a b = match a, b with | MInf, Int a | Int a, MInf -> MInf @@ -77,7 +79,7 @@ module VD : VALUE_DOMAIN = struct let subset a b = match a, b with | Bot, _ -> true | _, Bot -> false - | Itv(a, b), Itv(c, d) -> bound_leq a c && bound_leq d b + | Itv(a, b), Itv(c, d) -> bound_leq c a && bound_leq b d let join a b = match a, b with | Bot, x | x, Bot -> x @@ -96,12 +98,12 @@ module VD : VALUE_DOMAIN = struct | x, Bot | Bot, x -> x | Itv(a, b), Itv(c, d) -> let lb = - if not (bound_leq a c) then + if bound_lt c a then (if bound_leq (Int 0) c then Int 0 else MInf) else a in let ub = - if not (bound_leq d b) then + if bound_lt b d then (if bound_leq d (Int 0) then Int 0 else PInf) else b in |