diff options
Diffstat (limited to 'abstract/constant_domain.ml')
| -rw-r--r-- | abstract/constant_domain.ml | 25 |
1 files changed, 19 insertions, 6 deletions
diff --git a/abstract/constant_domain.ml b/abstract/constant_domain.ml index d142228..44a13fc 100644 --- a/abstract/constant_domain.ml +++ b/abstract/constant_domain.ml @@ -9,7 +9,7 @@ module Constants : VALUE_DOMAIN = struct let top = Top let bottom = Bot let const i = Int i - let rand i j = if i <> j then Top else Int i + let rand i j = if i > j then Bot else if i <> j then Top else Int i let subset a b = match a, b with | _, Top -> true @@ -27,7 +27,7 @@ module Constants : VALUE_DOMAIN = struct | Int a, Int b when a = b -> Int a | _ -> Bot - let widen = meet (* pas besoin d'accélerer la convergence au-delà *) + let widen = join (* pas besoin d'accélerer la convergence au-delà *) let neg = function | Int a -> Int (Z.neg a) @@ -39,13 +39,26 @@ module Constants : VALUE_DOMAIN = struct | _ -> Top let add = b_aux Z.add let sub = b_aux Z.sub - let mul = b_aux Z.mul - let div = b_aux Z.div - let rem = b_aux Z.rem + let mul a b = match a, b with + | Int x, Int y -> Int (Z.mul x y) + | Bot, _ | _, Bot -> Bot + | Int x, _ when x = Z.zero -> Int Z.zero + | _, Int x when x = Z.zero -> Int (Z.zero) + | _ -> Top + let div a b = match a, b with + | Int x, Int y -> Int (Z.div x y) + | Bot, _ | _, Bot -> Bot + | Int x, _ when x = Z.zero -> Int Z.zero + | _ -> Top + let rem a b = match a, b with + | Int x, Int y -> Int (Z.rem x y) + | Bot, _ | _, Bot -> Bot + | Int x, _ when x = Z.zero -> Int Z.zero + | _ -> Top let leq a b = match a, b with - | Int a, Int b when Z.leq a b -> + | Int a, Int b -> if Z.leq a b then Int a, Int b else Bot, Bot |