diff options
Diffstat (limited to 'abstract/nonrelational.ml')
| -rw-r--r-- | abstract/nonrelational.ml | 38 |
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 |