From 652d04c5476fdfb9cc7a2d93de3df4d76a6882ce Mon Sep 17 00:00:00 2001
From: Alex AUVOLAT <alex.auvolat@ens.fr>
Date: Sun, 1 Jun 2014 10:06:35 +0200
Subject: =?UTF-8?q?Impl=C3=A9mentation=20des=20intervalles=20;=20d=C3=A9bu?=
 =?UTF-8?q?t=20r=C3=A9daction=20du=20rapport.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 abstract/interpret.ml        |  1 -
 abstract/intervals_domain.ml | 41 +++++++++++++++++++++++++++++++++++++++--
 abstract/nonrelational.ml    |  2 +-
 3 files changed, 40 insertions(+), 4 deletions(-)

(limited to 'abstract')

diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index cb32e22..f6a6cb4 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -73,7 +73,6 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
                 (binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1))
                 env
 
-
         | _ -> env
         end
 
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml
index b63f8a9..d95a938 100644
--- a/abstract/intervals_domain.ml
+++ b/abstract/intervals_domain.ml
@@ -33,6 +33,21 @@ module Intervals : VALUE_DOMAIN = struct
         | Int(x), Int(y) -> Int(Z.mul x y)
         | MInf, PInf | PInf, MInf -> MInf
         | MInf, MInf | PInf, PInf -> PInf
+	let bound_div a b =
+		match a, b with
+		| _, PInf | _, MInf -> Int Z.zero
+		| PInf, Int i ->
+			if i < Z.zero then MInf
+			else PInf
+		| MInf, Int i ->
+			if i < Z.zero then PInf
+			else MInf
+		| Int i, Int j ->
+			if j = Z.zero then
+				if i < Z.zero then MInf
+				else PInf
+			else Int (Z.div i j)
+
 
     let bound_min a b = match a, b with
         | MInf, _ | _, MInf -> MInf
@@ -50,6 +65,8 @@ module Intervals : VALUE_DOMAIN = struct
         | PInf -> MInf
         | MInf -> PInf
         | Int i -> Int (Z.neg i)
+	
+	let bound_abs a = bound_max a (bound_neg a)
 
     (* implementation *)
     let top = Itv(MInf, PInf)
@@ -101,8 +118,28 @@ module Intervals : VALUE_DOMAIN = struct
                             (bound_max (bound_mul b c) (bound_mul b d))))
         
 
-    let div a b = top (* TODO *)
-    let rem a b = top (* TODO *)
+    let div a b = match a, b with
+        | Bot, _ -> Bot
+        | Itv(a, b), q ->
+			let p1 = match meet q (Itv(Int (Z.of_int 1), PInf)) with
+				| Bot -> Bot
+				| Itv(c, d) ->
+					Itv(min (bound_div a c) (bound_div a d), max (bound_div b c) (bound_div b d))
+			in
+			let p2 = match meet q (Itv(MInf, Int (Z.of_int (-1)))) with
+				| Bot -> Bot
+				| Itv(c, d) ->
+					Itv(min (bound_div b c) (bound_div b d), max (bound_div a c) (bound_div a d))
+			in
+			join p1 p2
+
+    let rem a b = match a, b with
+        | Bot, _ | _, Bot -> Bot
+        | Itv(a, b), Itv(c, d) ->
+			Itv(
+				Int Z.zero,
+				bound_max (bound_abs c) (bound_abs d)
+			)
 
     let leq a b = match a, b with
         | Bot, _ | _, Bot -> Bot, Bot
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index aa34d14..188c8bc 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -110,7 +110,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
         | Env m, Env n ->
             VarMap.for_all2o
                 (fun _ _ -> true)
-                (fun _ _ -> true)
+                (fun _ v -> v = V.top)
                 (fun _ a b -> V.subset a b)
                 m n
         
-- 
cgit v1.2.3