diff options
Diffstat (limited to 'abstract/nonrelational.ml')
| -rw-r--r-- | abstract/nonrelational.ml | 12 |
1 files changed, 7 insertions, 5 deletions
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 |