From 4204d25a2d277af1c16f55ee488e42c7b79bba1f Mon Sep 17 00:00:00 2001 From: Alex AUVOLAT Date: Wed, 21 May 2014 17:57:06 +0200 Subject: All tests pass except one ! --- abstract/nonrelational.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'abstract/nonrelational.ml') diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index 7221df1..8ac6a2a 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -61,31 +61,33 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct let assign x id expr = strict_apply (fun env -> Env (VarMap.add id (eval env expr) env)) x - let compare x e1 e2 = + 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' = V.leq v1 v2 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' = V.leq v1 v2 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' = V.leq v1 v2 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' = V.leq v1 v2 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 -- cgit v1.2.3