Just retab (many lines changed for nothing)

6 files changed, 450 insertions, 450 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
diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
index 5c00fbd..404548c 100644
--- a/abstract/environment_domain.ml
+++ b/abstract/environment_domain.ml
@@ -1,33 +1,33 @@
 open Abstract_syntax_tree
 
 module type ENVIRONMENT_DOMAIN = sig
-	type t
+    type t
 
-	(* construction *)
-	val init	: t
-	val bottom	: t
-	val is_bot  : t -> bool
+    (* construction *)
+    val init    : t
+    val bottom  : t
+    val is_bot  : t -> bool
 
-	(* variable management *)
-	val addvar	: t -> id -> t
-	val rmvar	: t -> id -> t
-	val vars	: t -> id list
+    (* variable management *)
+    val addvar  : t -> id -> t
+    val rmvar   : t -> id -> t
+    val vars    : t -> id list
 
-	(* abstract operation *)
-	val assign	: t -> id -> expr ext -> t		(*    S[id <- expr]     *)
-	val compare_leq : t -> expr ext -> expr ext -> t    (*    S[expr <= expr ?] *)
-	val compare_eq : t -> expr ext -> expr ext -> t    (*    S[expr = expr ?] *)
+    (* abstract operation *)
+    val assign  : t -> id -> expr ext -> t      (*    S[id <- expr]     *)
+    val compare_leq : t -> expr ext -> expr ext -> t    (*    S[expr <= expr ?] *)
+    val compare_eq : t -> expr ext -> expr ext -> t    (*    S[expr = expr ?] *)
 
-	(* set-theoretic operations *)
-	val join 	: t -> t -> t		(* union *)
-	val meet	: t -> t -> t		(* intersection *)
-	val widen	: t -> t -> t
+    (* set-theoretic operations *)
+    val join    : t -> t -> t       (* union *)
+    val meet    : t -> t -> t       (* intersection *)
+    val widen   : t -> t -> t
 
-	(* order *)
-	val subset	: t -> t -> bool
+    (* order *)
+    val subset  : t -> t -> bool
 
-	(* pretty-printing *)
-	val var_str	: t -> id list -> string
+    (* pretty-printing *)
+    val var_str : t -> id list -> string
 end
 
 
diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index 5f03775..c599a76 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -4,94 +4,94 @@ open Util
 
 module Make (E : ENVIRONMENT_DOMAIN) = struct
 
-	let neg (e, l) =
-		(AST_unary(AST_NOT, (e, l))), l
+    let neg (e, l) =
+        (AST_unary(AST_NOT, (e, l))), l
 
-	let binop op (e, l) e2 =
-		(AST_binary (op, (e,l), e2)), l
-	let m1 (e, l) =
-		binop AST_MINUS (e, l) (AST_int_const("1", l), l)
-	let p1 (e, l) =
-		binop AST_PLUS (e, l) (AST_int_const("1", l), l)
+    let binop op (e, l) e2 =
+        (AST_binary (op, (e,l), e2)), l
+    let m1 (e, l) =
+        binop AST_MINUS (e, l) (AST_int_const("1", l), l)
+    let p1 (e, l) =
+        binop AST_PLUS (e, l) (AST_int_const("1", l), l)
 
     let bottom_with_vars =
         List.fold_left E.addvar E.bottom
 
-	let rec condition cond env =
-		begin match fst cond with
-		| AST_binary (AST_LESS_EQUAL, e1, e2) ->
-			E.compare_leq env e1 e2
-		| AST_binary (AST_EQUAL, e1, e2) ->
+    let rec condition cond env =
+        begin match fst cond with
+        | AST_binary (AST_LESS_EQUAL, e1, e2) ->
+            E.compare_leq env e1 e2
+        | AST_binary (AST_EQUAL, e1, e2) ->
             E.compare_eq env e1 e2
-		| AST_binary (AST_AND, e1, e2) ->
-			E.meet (condition e1 env) (condition e2 env)
-		| AST_binary (AST_OR, e1, e2) ->
-			E.join (condition e1 env) (condition e2 env)
+        | AST_binary (AST_AND, e1, e2) ->
+            E.meet (condition e1 env) (condition e2 env)
+        | AST_binary (AST_OR, e1, e2) ->
+            E.join (condition e1 env) (condition e2 env)
 
-		(* transformations : remove not *)
-		| AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), x)) ->
-			condition cond env
-		| AST_unary (AST_NOT, (AST_binary(AST_AND, e1, e2), x)) ->
-			condition
-				(AST_binary(AST_OR, neg e1, neg e2), x) env
-		| AST_unary (AST_NOT, (AST_binary(AST_OR, e1, e2), x)) ->
-			condition
-				(AST_binary(AST_AND, neg e1, neg e2), x) env
+        (* transformations : remove not *)
+        | AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), x)) ->
+            condition cond env
+        | AST_unary (AST_NOT, (AST_binary(AST_AND, e1, e2), x)) ->
+            condition
+                (AST_binary(AST_OR, neg e1, neg e2), x) env
+        | AST_unary (AST_NOT, (AST_binary(AST_OR, e1, e2), x)) ->
+            condition
+                (AST_binary(AST_AND, neg e1, neg e2), x) env
 
-		| AST_unary (AST_NOT, (AST_binary(op, e1, e2), x)) ->
-			let op2 = match op with
-			| AST_LESS_EQUAL -> AST_GREATER
-			| AST_LESS -> AST_GREATER_EQUAL
-			| AST_GREATER_EQUAL -> AST_LESS
-			| AST_GREATER -> AST_LESS_EQUAL
-			| AST_EQUAL -> AST_NOT_EQUAL
-			| AST_NOT_EQUAL -> AST_EQUAL
-			| _ -> assert false
-			in
-			condition (binop op2 e1 e2) env
-		
-		(* transformations : encode everything with leq *)
-		| AST_binary(AST_LESS, e1, e2) ->
-			condition
-				(binop AST_AND (binop AST_LESS_EQUAL e1 (m1 e2))
-							   (binop AST_LESS_EQUAL (p1 e1) e2))
-				env
-		| AST_binary (AST_GREATER_EQUAL, e1, e2) ->
-			condition
-				(binop AST_LESS_EQUAL e2 e1)
-				env
-		| AST_binary (AST_GREATER, e1, e2) ->
-			condition
-				(binop AST_LESS e2 e1)
-				env
-		| AST_binary (AST_NOT_EQUAL, e1, e2) ->
-			condition
-				(binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1))
-				env
+        | AST_unary (AST_NOT, (AST_binary(op, e1, e2), x)) ->
+            let op2 = match op with
+            | AST_LESS_EQUAL -> AST_GREATER
+            | AST_LESS -> AST_GREATER_EQUAL
+            | AST_GREATER_EQUAL -> AST_LESS
+            | AST_GREATER -> AST_LESS_EQUAL
+            | AST_EQUAL -> AST_NOT_EQUAL
+            | AST_NOT_EQUAL -> AST_EQUAL
+            | _ -> assert false
+            in
+            condition (binop op2 e1 e2) env
+        
+        (* transformations : encode everything with leq *)
+        | AST_binary(AST_LESS, e1, e2) ->
+            condition
+                (binop AST_AND (binop AST_LESS_EQUAL e1 (m1 e2))
+                               (binop AST_LESS_EQUAL (p1 e1) e2))
+                env
+        | AST_binary (AST_GREATER_EQUAL, e1, e2) ->
+            condition
+                (binop AST_LESS_EQUAL e2 e1)
+                env
+        | AST_binary (AST_GREATER, e1, e2) ->
+            condition
+                (binop AST_LESS e2 e1)
+                env
+        | AST_binary (AST_NOT_EQUAL, e1, e2) ->
+            condition
+                (binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1))
+                env
 
-		| _ -> env
-		end
+        | _ -> env
+        end
 
-	let rec interp_stmt env stat =
-		begin match fst stat with
-		| AST_block b ->
-			(* remember to remove vars that have gone out of scope at the end *)
-			let prevars = E.vars env in
-			let env2 = List.fold_left interp_stmt env b in
-			let postvars = E.vars env2 in
-			let rmvars = List.filter (fun x -> not (List.mem x prevars)) postvars in
-			List.fold_left E.rmvar env2 rmvars
-		| AST_assign ((id, _), exp) ->
-			E.assign env id exp
-		| AST_if (cond, tb, None) ->
-			E.join
-				(interp_stmt (condition cond env) tb)
-				(condition (neg cond) env)
-		| AST_if (cond, tb, Some eb) ->
-			let e1 = (interp_stmt (condition cond env) tb) in
-			let e2 = (interp_stmt (condition (neg cond) env) eb) in
-			E.join e1 e2
-		| AST_while (cond, body) ->
+    let rec interp_stmt env stat =
+        begin match fst stat with
+        | AST_block b ->
+            (* remember to remove vars that have gone out of scope at the end *)
+            let prevars = E.vars env in
+            let env2 = List.fold_left interp_stmt env b in
+            let postvars = E.vars env2 in
+            let rmvars = List.filter (fun x -> not (List.mem x prevars)) postvars in
+            List.fold_left E.rmvar env2 rmvars
+        | AST_assign ((id, _), exp) ->
+            E.assign env id exp
+        | AST_if (cond, tb, None) ->
+            E.join
+                (interp_stmt (condition cond env) tb)
+                (condition (neg cond) env)
+        | AST_if (cond, tb, Some eb) ->
+            let e1 = (interp_stmt (condition cond env) tb) in
+            let e2 = (interp_stmt (condition (neg cond) env) eb) in
+            E.join e1 e2
+        | AST_while (cond, body) ->
             (* loop unrolling *)
             let rec unroll u = function
                 | 0 -> u, bottom_with_vars (E.vars env)
@@ -118,40 +118,40 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
             let x = iter 0 env in
             let y = fix fsharp x in     (* decreasing iteration *)
             E.join (condition (neg cond) y) u_u
-		| AST_HALT -> bottom_with_vars (E.vars env)
-		| AST_assert cond ->
-			if not
-				(E.is_bot (condition (neg cond) env))
-			then begin
-				Format.printf "%s: ERROR: assertion failure@."
-					(Abstract_syntax_printer.string_of_extent (snd stat));
-			end;
-			condition cond env
-		| AST_print items ->
-			Format.printf "%s: %s@."
-				(Abstract_syntax_printer.string_of_extent (snd stat))
-				(E.var_str env (List.map fst items));
-			env
-		| AST_local ((ty, _), vars) ->
-			List.fold_left
-				(fun env ((id, _), init) ->
-					let env2 = E.addvar env id in
-					match init with
-					| Some e -> E.assign env2 id e
-					| None -> env2)
-				env
-				vars
-		| _ -> assert false (* not implemented *)
-		end
-	
-	let interpret prog =
-		let result = List.fold_left
-			(fun env x -> match x with
-				| AST_stat st -> interp_stmt env st
-				| _ -> env)
-			E.init
-			(fst prog)
-		in
-			Format.printf "Output: %s@."
-				(E.var_str result (E.vars result))
+        | AST_HALT -> bottom_with_vars (E.vars env)
+        | AST_assert cond ->
+            if not
+                (E.is_bot (condition (neg cond) env))
+            then begin
+                Format.printf "%s: ERROR: assertion failure@."
+                    (Abstract_syntax_printer.string_of_extent (snd stat));
+            end;
+            condition cond env
+        | AST_print items ->
+            Format.printf "%s: %s@."
+                (Abstract_syntax_printer.string_of_extent (snd stat))
+                (E.var_str env (List.map fst items));
+            env
+        | AST_local ((ty, _), vars) ->
+            List.fold_left
+                (fun env ((id, _), init) ->
+                    let env2 = E.addvar env id in
+                    match init with
+                    | Some e -> E.assign env2 id e
+                    | None -> env2)
+                env
+                vars
+        | _ -> assert false (* not implemented *)
+        end
+    
+    let interpret prog =
+        let result = List.fold_left
+            (fun env x -> match x with
+                | AST_stat st -> interp_stmt env st
+                | _ -> env)
+            E.init
+            (fst prog)
+        in
+            Format.printf "Output: %s@."
+                (E.var_str result (E.vars result))
 end
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml
index 98f4daf..b63f8a9 100644
--- a/abstract/intervals_domain.ml
+++ b/abstract/intervals_domain.ml
@@ -1,122 +1,122 @@
 open Value_domain
 
 module Intervals : VALUE_DOMAIN = struct
-  type bound = Int of Z.t | PInf | MInf
-
-  type t = Itv of bound * bound | Bot
-
-  (* utilities *)
-  let bound_leq a b =   (* a <= b ? *)
-    match a, b with
-    | MInf, _ | _, PInf -> true
-    | Int a, Int b -> Z.leq a b
-    | x, y -> x = y
-
-  let bound_add a b =
-    match a, b with
-    | MInf, Int a | Int a, MInf -> MInf
-    | PInf, Int a | Int a, PInf -> PInf
-    | MInf, MInf -> MInf
-    | PInf, PInf -> PInf
-    | Int a, Int b -> Int (Z.add a b)
-    | _ -> assert false
-  let bound_mul a b =
-    match a, b with
-    | PInf, Int(x) | Int(x), PInf ->
-      if x > Z.zero then PInf
-      else if x < Z.zero then MInf
-      else Int Z.zero
-    | MInf, Int(x) | Int(x), MInf ->
-      if x < Z.zero then PInf
-      else if x > Z.zero then MInf
-      else Int Z.zero
-    | Int(x), Int(y) -> Int(Z.mul x y)
-    | MInf, PInf | PInf, MInf -> MInf
-    | MInf, MInf | PInf, PInf -> PInf
-
-  let bound_min a b = match a, b with
-    | MInf, _ | _, MInf -> MInf
-    | Int a, Int b -> Int (min a b)
-    | Int a, PInf -> Int a
-    | PInf, Int a -> Int a
-    | PInf, PInf -> PInf
-  let bound_max a b = match a, b with
-    | PInf, _ | _, PInf -> PInf
-    | Int a, Int b -> Int (max a b)
-    | Int a, MInf | MInf, Int a -> Int a
-    | MInf, MInf -> MInf
-
-  let bound_neg = function
-    | PInf -> MInf
-    | MInf -> PInf
-    | Int i -> Int (Z.neg i)
-
-  (* implementation *)
-  let top = Itv(MInf, PInf)
-  let bottom = Bot
-  let const i = Itv(Int i, Int i)
-  let rand i j =
+    type bound = Int of Z.t | PInf | MInf
+
+    type t = Itv of bound * bound | Bot
+
+    (* utilities *)
+    let bound_leq a b =   (* a <= b ? *)
+        match a, b with
+        | MInf, _ | _, PInf -> true
+        | Int a, Int b -> Z.leq a b
+        | x, y -> x = y
+
+    let bound_add a b =
+        match a, b with
+        | MInf, Int a | Int a, MInf -> MInf
+        | PInf, Int a | Int a, PInf -> PInf
+        | MInf, MInf -> MInf
+        | PInf, PInf -> PInf
+        | Int a, Int b -> Int (Z.add a b)
+        | _ -> assert false
+    let bound_mul a b =
+        match a, b with
+        | PInf, Int(x) | Int(x), PInf ->
+            if x > Z.zero then PInf
+            else if x < Z.zero then MInf
+            else Int Z.zero
+        | MInf, Int(x) | Int(x), MInf ->
+            if x < Z.zero then PInf
+            else if x > Z.zero then MInf
+            else Int Z.zero
+        | Int(x), Int(y) -> Int(Z.mul x y)
+        | MInf, PInf | PInf, MInf -> MInf
+        | MInf, MInf | PInf, PInf -> PInf
+
+    let bound_min a b = match a, b with
+        | MInf, _ | _, MInf -> MInf
+        | Int a, Int b -> Int (min a b)
+        | Int a, PInf -> Int a
+        | PInf, Int a -> Int a
+        | PInf, PInf -> PInf
+    let bound_max a b = match a, b with
+        | PInf, _ | _, PInf -> PInf
+        | Int a, Int b -> Int (max a b)
+        | Int a, MInf | MInf, Int a -> Int a
+        | MInf, MInf -> MInf
+
+    let bound_neg = function
+        | PInf -> MInf
+        | MInf -> PInf
+        | Int i -> Int (Z.neg i)
+
+    (* implementation *)
+    let top = Itv(MInf, PInf)
+    let bottom = Bot
+    let const i = Itv(Int i, Int i)
+    let rand i j =
     if Z.leq i j then Itv(Int i, Int j) else Bot
 
-  let subset a b = match a, b with
-    | Bot, _ -> true
-    | _, Bot -> false
-    | Itv(a, b), Itv(c, d) -> bound_leq a c && bound_leq d b
-
-  let join a b = match a, b with
-    | Bot, x | x, Bot -> x
-    | Itv(a, b), Itv(c, d) -> Itv(bound_min a c, bound_max b d)
-
-  let meet a b = match a, b with
-    | Bot, x | x, Bot -> Bot
-    | Itv(a, b), Itv(c, d) ->
-      let u, v = bound_max a c, bound_min b d in
-      if bound_leq u v
-        then Itv(u, v)
-        else Bot
-
-  let widen a b = match a, b with
-    | x, Bot | Bot, x -> x
-    | Itv(a, b), Itv(c, d) ->
-      Itv(
-        (if not (bound_leq a c) then MInf else a),
-        (if not (bound_leq d b) then PInf else b))
-
-  let neg = function
-    | Bot -> Bot
-    | Itv(a, b) -> Itv(bound_neg b, bound_neg a)
-  let add a b = match a, b with
-    | Bot, _ | _, Bot -> Bot
-    | Itv(a, b), Itv(c, d) -> Itv(bound_add a c, bound_add b d)
-  let sub a b = match a, b with
-    | Bot, _ | _, Bot -> Bot
-    | Itv(a, b), Itv(c, d) -> Itv(bound_add a (bound_neg d), bound_add b (bound_neg c))
-  let mul a b = match a, b with
-    | Bot, _ | _, Bot -> Bot
-    | Itv(a, b), Itv(c, d) ->
-        Itv(
-          (bound_min (bound_min (bound_mul a c) (bound_mul a d))
-                     (bound_min (bound_mul b c) (bound_mul b d))),
-          (bound_max (bound_max (bound_mul a c) (bound_mul a d))
-                     (bound_max (bound_mul b c) (bound_mul b d))))
-      
-
-  let div a b = top (* TODO *)
-  let rem a b = top (* TODO *)
-
-  let leq a b = match a, b with
-    | Bot, _ | _, Bot -> Bot, Bot
-    | Itv(a, b), Itv(c, d) ->
-      if not (bound_leq a d)
-        then Bot, Bot
-        else Itv(a, bound_min b d), Itv(bound_max a c, d)
-
-  let bound_str = function
-    | MInf -> "-oo"
-    | PInf -> "+oo"
-    | Int i -> Z.to_string i
-  let to_string = function
-    | Bot -> "bot"
-    | Itv(a, b) -> "[" ^ (bound_str a) ^ ";" ^ (bound_str b) ^ "]"
+    let subset a b = match a, b with
+        | Bot, _ -> true
+        | _, Bot -> false
+        | Itv(a, b), Itv(c, d) -> bound_leq a c && bound_leq d b
+
+    let join a b = match a, b with
+        | Bot, x | x, Bot -> x
+        | Itv(a, b), Itv(c, d) -> Itv(bound_min a c, bound_max b d)
+
+    let meet a b = match a, b with
+        | Bot, x | x, Bot -> Bot
+        | Itv(a, b), Itv(c, d) ->
+            let u, v = bound_max a c, bound_min b d in
+            if bound_leq u v
+            then Itv(u, v)
+            else Bot
+
+    let widen a b = match a, b with
+        | x, Bot | Bot, x -> x
+        | Itv(a, b), Itv(c, d) ->
+            Itv(
+            (if not (bound_leq a c) then MInf else a),
+            (if not (bound_leq d b) then PInf else b))
+
+    let neg = function
+        | Bot -> Bot
+        | Itv(a, b) -> Itv(bound_neg b, bound_neg a)
+    let add a b = match a, b with
+        | Bot, _ | _, Bot -> Bot
+        | Itv(a, b), Itv(c, d) -> Itv(bound_add a c, bound_add b d)
+    let sub a b = match a, b with
+        | Bot, _ | _, Bot -> Bot
+        | Itv(a, b), Itv(c, d) -> Itv(bound_add a (bound_neg d), bound_add b (bound_neg c))
+    let mul a b = match a, b with
+        | Bot, _ | _, Bot -> Bot
+        | Itv(a, b), Itv(c, d) ->
+            Itv(
+                (bound_min (bound_min (bound_mul a c) (bound_mul a d))
+                            (bound_min (bound_mul b c) (bound_mul b d))),
+                (bound_max (bound_max (bound_mul a c) (bound_mul a d))
+                            (bound_max (bound_mul b c) (bound_mul b d))))
+        
+
+    let div a b = top (* TODO *)
+    let rem a b = top (* TODO *)
+
+    let leq a b = match a, b with
+        | Bot, _ | _, Bot -> Bot, Bot
+        | Itv(a, b), Itv(c, d) ->
+            if not (bound_leq a d)
+            then Bot, Bot
+            else Itv(a, bound_min b d), Itv(bound_max a c, d)
+
+    let bound_str = function
+        | MInf -> "-oo"
+        | PInf -> "+oo"
+        | Int i -> Z.to_string i
+    let to_string = function
+        | Bot -> "bot"
+        | Itv(a, b) -> "[" ^ (bound_str a) ^ ";" ^ (bound_str b) ^ "]"
 
 end
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 8ac6a2a..39095b0 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -6,130 +6,130 @@ open Environment_domain
 
 
 module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
-	type env = V.t VarMap.t
+    type env = V.t VarMap.t
 
-	type t = Env of env | Bot
+    type t = Env of env | Bot
 
-	let init = Env VarMap.empty
-	let bottom = Bot
+    let init = Env VarMap.empty
+    let bottom = Bot
 
-	let get_var env id =
-		try VarMap.find id env
-		with Not_found -> V.top
-	
-	(* utilities *)
+    let get_var env id =
+        try VarMap.find id env
+        with Not_found -> V.top
+    
+    (* utilities *)
 
-	let rec eval env expr =
-		begin match fst expr with
-		| AST_identifier (id, _) -> get_var env id
-		| AST_int_const (s, _) -> V.const (Z.of_string s)
-		| AST_int_rand ((s, _), (t, _)) -> V.rand (Z.of_string s) (Z.of_string t)
-		| AST_unary (AST_UNARY_PLUS, e) -> eval env e
-		| AST_unary (AST_UNARY_MINUS, e) -> V.neg (eval env e)
-		| AST_unary (_, e) -> V.bottom
-		| AST_binary (op, e1, e2) ->
-			let f = match op with
-			| AST_PLUS -> V.add
-			| AST_MINUS -> V.sub
-			| AST_MULTIPLY -> V.mul
-			| AST_DIVIDE -> V.div
-			| AST_MODULO -> V.rem
-			| _ -> fun _ _ -> V.bottom
-			in f (eval env e1) (eval env e2)
-		| _ -> assert false (* unimplemented extension *)
-		end
+    let rec eval env expr =
+        begin match fst expr with
+        | AST_identifier (id, _) -> get_var env id
+        | AST_int_const (s, _) -> V.const (Z.of_string s)
+        | AST_int_rand ((s, _), (t, _)) -> V.rand (Z.of_string s) (Z.of_string t)
+        | AST_unary (AST_UNARY_PLUS, e) -> eval env e
+        | AST_unary (AST_UNARY_MINUS, e) -> V.neg (eval env e)
+        | AST_unary (_, e) -> V.bottom
+        | AST_binary (op, e1, e2) ->
+            let f = match op with
+            | AST_PLUS -> V.add
+            | AST_MINUS -> V.sub
+            | AST_MULTIPLY -> V.mul
+            | AST_DIVIDE -> V.div
+            | AST_MODULO -> V.rem
+            | _ -> fun _ _ -> V.bottom
+            in f (eval env e1) (eval env e2)
+        | _ -> assert false (* unimplemented extension *)
+        end
 
-	let strict env =					(*		env -> t		*)
-		if VarMap.exists (fun _ x -> x = V.bottom) env
-			then Bot
-			else Env env
-	let strict_apply f = function		(* (env -> t) -> t -> t *)
-		| Bot -> Bot
-		| Env e -> match f e with
-			| Bot -> Bot
-			| Env e -> strict e
+    let strict env =                    (*      env -> t        *)
+        if VarMap.exists (fun _ x -> x = V.bottom) env
+            then Bot
+            else Env env
+    let strict_apply f = function       (* (env -> t) -> t -> t *)
+        | Bot -> Bot
+        | Env e -> match f e with
+            | Bot -> Bot
+            | Env e -> strict e
 
-	(* implementation *)
+    (* implementation *)
 
-	let is_bot env = match env with
-		| Bot -> true
-		| Env env -> strict env = Bot
+    let is_bot env = match env with
+        | Bot -> true
+        | Env env -> strict env = Bot
 
-	let addvar x id = strict_apply (fun y -> Env (VarMap.add id V.top y)) x
-	let rmvar x id = strict_apply (fun y -> Env (VarMap.remove id y)) x
+    let addvar x id = strict_apply (fun y -> Env (VarMap.add id V.top y)) x
+    let rmvar x id = strict_apply (fun y -> Env (VarMap.remove id y)) x
 
-	let assign x id expr = strict_apply
-		(fun env -> Env (VarMap.add id (eval env expr) env))
-		x
-	let compare f x e1 e2 =
-		strict_apply (fun env -> match fst e1, fst e2 with
-				| AST_identifier(a, _), AST_identifier(b, _) ->
-					let v1, v2 = get_var env a, get_var env b in
-					let v1', v2' = f v1 v2 in
-					Env (VarMap.add a v1' (VarMap.add b v2' env))
-				| AST_identifier(a, _), _ ->
-					let v1, v2 = get_var env a, eval env e2 in
-					let v1', v2' = f v1 v2 in
-					if V.bottom = v2'
-						then Bot
-						else Env (VarMap.add a v1' env)
-				| _, AST_identifier(b, _) ->
-					let v1, v2 = eval env e1, get_var env b in
-					let v1', v2' = f v1 v2 in
-					if V.bottom = v1'
-						then Bot
-						else Env (VarMap.add b v2' env)
-				| _ ->
-					let v1, v2 = eval env e1, eval env e2 in
-					let v1', v2' = f v1 v2 in
-					if V.bottom = v1' ||V.bottom = v2'
-						then Bot
-						else Env env)
-			x
+    let assign x id expr = strict_apply
+        (fun env -> Env (VarMap.add id (eval env expr) env))
+        x
+    let compare f x e1 e2 =
+        strict_apply (fun env -> match fst e1, fst e2 with
+                | AST_identifier(a, _), AST_identifier(b, _) ->
+                    let v1, v2 = get_var env a, get_var env b in
+                    let v1', v2' = f v1 v2 in
+                    Env (VarMap.add a v1' (VarMap.add b v2' env))
+                | AST_identifier(a, _), _ ->
+                    let v1, v2 = get_var env a, eval env e2 in
+                    let v1', v2' = f v1 v2 in
+                    if V.bottom = v2'
+                        then Bot
+                        else Env (VarMap.add a v1' env)
+                | _, AST_identifier(b, _) ->
+                    let v1, v2 = eval env e1, get_var env b in
+                    let v1', v2' = f v1 v2 in
+                    if V.bottom = v1'
+                        then Bot
+                        else Env (VarMap.add b v2' env)
+                | _ ->
+                    let v1, v2 = eval env e1, eval env e2 in
+                    let v1', v2' = f v1 v2 in
+                    if V.bottom = v1' ||V.bottom = v2'
+                        then Bot
+                        else Env env)
+            x
     let compare_leq = compare V.leq
     let compare_eq = compare (fun x y -> let r = V.meet x y in r, r)
 
-	let join a b = match a, b with
-		| Bot, x | x, Bot -> x
-		| Env m, Env n ->
-			strict (VarMap.map2z (fun _ a b -> V.join a b) m n)
-	
-	let meet a b = match a, b with
-		| Bot, _ | _, Bot -> Bot
-		| Env m, Env n ->
-			strict (VarMap.map2z (fun _ a b -> V.meet a b) m n)
+    let join a b = match a, b with
+        | Bot, x | x, Bot -> x
+        | Env m, Env n ->
+            strict (VarMap.map2z (fun _ a b -> V.join a b) m n)
+    
+    let meet a b = match a, b with
+        | Bot, _ | _, Bot -> Bot
+        | Env m, Env n ->
+            strict (VarMap.map2z (fun _ a b -> V.meet a b) m n)
 
-	let widen a b = match a, b with
-		| Bot, x | x, Bot -> x
-		| Env m, Env n ->
-			strict (VarMap.map2z (fun _ a b -> V.widen a b) m n)
-	
-	let subset a b = match a, b with
-		| Bot, x -> true
-		| Env _, Bot -> false
-		| Env m, Env n ->
-			VarMap.for_all2o
-				(fun _ _ -> true)
-				(fun _ _ -> true)
-				(fun _ a b -> V.subset a b)
-				m n
-		
-	(* pretty-printing *)
-	let var_str env vars =
-		match env with
-		| Bot -> "bottom"
-		| Env env ->
-			let v = List.fold_left
-				(fun s id ->
-					(if s = "" then s else s ^ ", ") ^
-						id ^ " in " ^ (V.to_string (get_var env id))
-					)
-				""
-				vars
-			in
-				"[ " ^ v ^ " ]"
-	
-	let vars env = match env with
-		| Bot -> []
-		| Env env -> List.map fst (VarMap.bindings env)
+    let widen a b = match a, b with
+        | Bot, x | x, Bot -> x
+        | Env m, Env n ->
+            strict (VarMap.map2z (fun _ a b -> V.widen a b) m n)
+    
+    let subset a b = match a, b with
+        | Bot, x -> true
+        | Env _, Bot -> false
+        | Env m, Env n ->
+            VarMap.for_all2o
+                (fun _ _ -> true)
+                (fun _ _ -> true)
+                (fun _ a b -> V.subset a b)
+                m n
+        
+    (* pretty-printing *)
+    let var_str env vars =
+        match env with
+        | Bot -> "bottom"
+        | Env env ->
+            let v = List.fold_left
+                (fun s id ->
+                    (if s = "" then s else s ^ ", ") ^
+                        id ^ " in " ^ (V.to_string (get_var env id))
+                    )
+                ""
+                vars
+            in
+                "[ " ^ v ^ " ]"
+    
+    let vars env = match env with
+        | Bot -> []
+        | Env env -> List.map fst (VarMap.bindings env)
 end
diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml
index 9cf6d76..da4f481 100644
--- a/abstract/value_domain.ml
+++ b/abstract/value_domain.ml
@@ -1,31 +1,31 @@
 module type VALUE_DOMAIN = sig
-	type t
+    type t
 
-	(* constructors *)
-	val top		: t
-	val bottom	: t
-	val const	: Z.t -> t
-	val rand	: Z.t -> Z.t -> t
+    (* constructors *)
+    val top     : t
+    val bottom  : t
+    val const   : Z.t -> t
+    val rand    : Z.t -> Z.t -> t
 
-	(* order *)
-	val subset	: t -> t -> bool
+    (* order *)
+    val subset  : t -> t -> bool
 
-	(* set-theoretic operations *)
-	val join	: t -> t -> t   (* union *)
-	val meet	: t -> t -> t	(* intersection *)
-	val widen	: t -> t -> t
+    (* set-theoretic operations *)
+    val join    : t -> t -> t   (* union *)
+    val meet    : t -> t -> t   (* intersection *)
+    val widen   : t -> t -> t
 
-	(* arithmetic operations *)
-	val neg		: t -> t
-	val add		: t -> t -> t
-	val sub		: t -> t -> t
-	val mul		: t -> t -> t
-	val div		: t -> t -> t
-	val rem		: t -> t -> t
+    (* arithmetic operations *)
+    val neg     : t -> t
+    val add     : t -> t -> t
+    val sub     : t -> t -> t
+    val mul     : t -> t -> t
+    val div     : t -> t -> t
+    val rem     : t -> t -> t
 
-	(* boolean test *)
-	val leq		: t -> t -> t * t	(* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *)
+    (* boolean test *)
+    val leq     : t -> t -> t * t   (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *)
 
-	(* pretty-printing *)
-	val to_string : t -> string
+    (* pretty-printing *)
+    val to_string : t -> string
 end