diff --git a/infer/src/checkers/abstractDomain.ml b/infer/src/checkers/abstractDomain.ml index 7b06a3d66..19b97dafd 100644 --- a/infer/src/checkers/abstractDomain.ml +++ b/infer/src/checkers/abstractDomain.ml @@ -12,47 +12,47 @@ module F = Format module type AbstractDomain = sig type astate - val init : astate (* the initial state *) - val bot : astate - val is_bot : astate -> bool - val lteq : lhs:astate -> rhs:astate -> bool (* fst \sqsubseteq snd? *) + val initial : astate + val bottom : astate + val is_bottom : astate -> bool + val (<=) : lhs:astate -> rhs:astate -> bool (* fst \sqsubseteq snd? *) val join : astate -> astate -> astate val widen : prev:astate -> next:astate -> num_iters:int -> astate val pp : F.formatter -> astate -> unit end -module BotLiftedAbstractDomain (A : AbstractDomain) : AbstractDomain = struct +module BottomLiftedAbstractDomain (A : AbstractDomain) : AbstractDomain = struct type astate = - | Bot - | NonBot of A.astate + | Bottom + | NonBottom of A.astate - let bot = Bot + let bottom = Bottom - let is_bot astate = - astate = Bot + let is_bottom astate = + astate = Bottom - let init = NonBot A.init + let initial = NonBottom A.initial - let lteq ~lhs ~rhs = match lhs, rhs with - | Bot, _ -> true - | _ , Bot -> false - | NonBot lhs, NonBot rhs -> A.lteq ~lhs ~rhs + let (<=) ~lhs ~rhs = match lhs, rhs with + | Bottom, _ -> true + | _ , Bottom -> false + | NonBottom lhs, NonBottom rhs -> A.(<=) ~lhs ~rhs let join astate1 astate2 = match astate1, astate2 with - | Bot, _ -> astate2 - | _, Bot -> astate1 - | NonBot a1, NonBot a2 -> NonBot (A.join a1 a2) + | Bottom, _ -> astate2 + | _, Bottom -> astate1 + | NonBottom a1, NonBottom a2 -> NonBottom (A.join a1 a2) let widen ~prev ~next ~num_iters = match prev, next with - | Bot, _ -> next - | _, Bot -> prev - | NonBot prev, NonBot next -> NonBot (A.widen ~prev ~next ~num_iters) + | Bottom, _ -> next + | _, Bottom -> prev + | NonBottom prev, NonBottom next -> NonBottom (A.widen ~prev ~next ~num_iters) let pp fmt = function - | Bot -> F.fprintf fmt "_|_" - | NonBot astate -> A.pp fmt astate + | Bottom -> F.fprintf fmt "_|_" + | NonBottom astate -> A.pp fmt astate end diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml index 36b83aef3..5335d7a69 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/infer/src/checkers/abstractInterpreter.ml @@ -36,7 +36,7 @@ module Make let old_state = M.find node_id inv_map in let widened_post = A.widen ~prev:old_state.post ~next:astate_post ~num_iters:old_state.visit_count in - if A.lteq ~lhs:widened_post ~rhs:old_state.post + if A.(<=) ~lhs:widened_post ~rhs:old_state.post then begin L.out "Old state contains new, not adding succs@."; @@ -65,7 +65,7 @@ module Make let join_pred astate_acc pred_id = let pred_state = M.find pred_id inv_map in A.join pred_state.post astate_acc in - let astate_pre = IList.fold_left join_pred A.bot visited_preds in + let astate_pre = IList.fold_left join_pred A.bottom visited_preds in let inv_map', work_queue'' = exec_node node astate_pre work_queue' inv_map in exec_worklist work_queue'' inv_map' | None -> inv_map @@ -74,7 +74,7 @@ module Make L.out "Starting analysis of %a@." Procname.pp (Cfg.Procdesc.get_proc_name pdesc); let cfg = C.from_pdesc pdesc in let start_node = C.start_node cfg in - let inv_map', work_queue' = exec_node start_node A.init (S.empty cfg) M.empty in + let inv_map', work_queue' = exec_node start_node A.initial (S.empty cfg) M.empty in exec_worklist work_queue' inv_map' end diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml index 74cc5cd68..3bccb30ab 100644 --- a/infer/src/unit/abstractInterpreterTests.ml +++ b/infer/src/unit/abstractInterpreterTests.ml @@ -25,15 +25,15 @@ module PathCountDomain = struct then Top else PathCount c - let bot = make_path_count 0 + let bottom = make_path_count 0 - let init = make_path_count 1 + let initial = make_path_count 1 - let is_bot = function + let is_bottom = function | PathCount c -> c = 0 | Top -> false - let lteq ~lhs ~rhs = match lhs, rhs with + let (<=) ~lhs ~rhs = match lhs, rhs with | PathCount c1, PathCount c2 -> c1 <= c2 | _, Top -> true | Top, PathCount _ -> false diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index fbaa6f626..183133468 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -157,7 +157,7 @@ module Make try let state = M.find node_id inv_map in state.post - with Not_found -> A.bot in + with Not_found -> A.bottom in let post_str = pp_to_string A.pp node_id_post in if inv_str <> post_str then let error_msg =