Many things work!

1 files changed, 23 insertions, 15 deletions

diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index d4118da..7221df1 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -66,16 +66,25 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
 				| AST_identifier(a, _), AST_identifier(b, _) ->
 					let v1, v2 = get_var env a, get_var env b in
 					let v1', v2' = V.leq v1 v2 in
-					Env (VarMap.add a v1' (VarMap.add b v1' env))
-				| AST_identifier(a, _), AST_int_const(s, _) ->
-					let v1, v2 = get_var env a, V.const (Z.of_string s) in
-					let v1', _ = V.leq v1 v2 in
-					Env (VarMap.add a v1' env)
-				| AST_int_const(s, _), AST_identifier(b, _) ->
-					let v1, v2 = V.const (Z.of_string s), get_var env b in
-					let _, v2' = V.leq v1 v2 in
-					Env (VarMap.add b v2' env)
-				| _ -> Env env)
+					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' = V.leq 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' = V.leq 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' = V.leq v1 v2 in
+					if V.bottom = v1' ||V.bottom = v2'
+						then Bot
+						else Env env)
 			x
 
 	let join a b = match a, b with
@@ -106,7 +115,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
 	(* pretty-printing *)
 	let var_str env vars =
 		match env with
-		| Bot -> "bot"
+		| Bot -> "bottom"
 		| Env env ->
 			let v = List.fold_left
 				(fun s id ->
@@ -118,8 +127,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
 			in
 				"[ " ^ v ^ " ]"
 	
-	let all_vars_str env =
-		match env with
-		| Bot -> "bot"
-		| Env map -> var_str env (List.map fst (VarMap.bindings map))
+	let vars env = match env with
+		| Bot -> []
+		| Env env -> List.map fst (VarMap.bindings env)
 end