Many things work!

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