diff options
author | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-05-21 18:07:37 +0200 |
---|---|---|
committer | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-05-21 18:07:37 +0200 |
commit | 77df0b0f119fc70624e4b830320a2b3e1034f7b5 (patch) | |
tree | ebac7e6c6bd653359181af16cc71192138161f47 /abstract/constant_domain.ml | |
parent | 4204d25a2d277af1c16f55ee488e42c7b79bba1f (diff) | |
download | SemVerif-Projet-77df0b0f119fc70624e4b830320a2b3e1034f7b5.tar.gz SemVerif-Projet-77df0b0f119fc70624e4b830320a2b3e1034f7b5.zip |
Just retab (many lines changed for nothing)
Diffstat (limited to 'abstract/constant_domain.ml')
-rw-r--r-- | abstract/constant_domain.ml | 128 |
1 files changed, 64 insertions, 64 deletions
diff --git a/abstract/constant_domain.ml b/abstract/constant_domain.ml index 44a13fc..abc3aa0 100644 --- a/abstract/constant_domain.ml +++ b/abstract/constant_domain.ml @@ -1,71 +1,71 @@ 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 + 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 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 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) ^ "}" + 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 |