open Value_domain module Constants : VALUE_DOMAIN = struct type t = | Top | Int of Z.t | Bot let top = Top let bottom = Bot let const i = 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 | Bot, _ -> true | Int a, Int b -> a = b | _, _ -> false let join a b = match a, b with | Bot, x | x, Bot -> x | Int a, Int b when a = b -> Int a | _ -> Top let meet a b = match a, b with | Top, x | x, Top -> x | Int a, Int b when a = b -> Int a | _ -> Bot let widen = join (* pas besoin d'accélerer la convergence au-delà *) let neg = function | Int a -> Int (Z.neg a) | x -> x let b_aux op a b = match a, b with | Int x, Int y -> Int (op x y) | Bot, _ | _, Bot -> Bot | _ -> Top let add = b_aux Z.add let sub = b_aux Z.sub 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 -> if Z.leq a b then Int a, Int b else Bot, Bot | x, y -> x, y let to_string = function | Bot -> "bot" | Top -> "top" | Int i -> "{" ^ (Z.to_string i) ^ "}" end