diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 6e145171c..acdf5f0dd 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -172,7 +172,7 @@ module Init = struct in let mem = Dom.Mem.init in let mem, _ = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in - let formals = Sem.get_formals pdesc in + let formals = Dom.get_formals pdesc in declare_symbolic_parameters pname tenv integer_type_widths ~node_hash location symbol_table formals mem end @@ -216,7 +216,7 @@ module TransferFunctions = struct let ret_var = Loc.of_var (Var.of_id ret_id) in let ret_val = Dom.Mem.find (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem in let formals = - List.fold (Sem.get_formals callee_pdesc) ~init:PowLoc.bot ~f:(fun acc (formal, _) -> + List.fold (Dom.get_formals callee_pdesc) ~init:PowLoc.bot ~f:(fun acc (formal, _) -> let v = Dom.Mem.find (Loc.of_pvar formal) callee_exit_mem in PowLoc.join acc (Dom.Val.get_all_locs v) ) in @@ -308,7 +308,7 @@ module TransferFunctions = struct let pname = Procdesc.get_proc_name pdesc in match Typ.Procname.get_method pname with | "__inferbo_empty" when Loc.is_return loc_v -> ( - match Sem.get_formals pdesc with + match Dom.get_formals pdesc with | [(formal, _)] -> let formal_v = Dom.Mem.find (Loc.of_pvar formal) mem in Dom.Mem.store_empty_alias formal_v loc_v mem diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 272cb1f30..1c1edbb02 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -21,6 +21,12 @@ type eval_sym_trace = ; trace_of_sym: Symb.Symbol.t -> Trace.Set.t ; eval_locpath: PowLoc.eval_locpath } +let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list = + fun pdesc -> + let proc_name = Procdesc.get_proc_name pdesc in + Procdesc.get_formals pdesc |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ)) + + module Val = struct type t = { itv: Itv.t diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index ecbce1f21..2c5c18b01 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -296,12 +296,6 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t = Val.bot -let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list = - fun pdesc -> - let proc_name = Procdesc.get_proc_name pdesc in - Procdesc.get_formals pdesc |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ)) - - module ParamBindings = struct include PrettyPrintable.MakePPMap (struct include Pvar diff --git a/infer/src/checkers/reachingDefs.ml b/infer/src/checkers/reachingDefs.ml index ac850ccee..d07733c7a 100644 --- a/infer/src/checkers/reachingDefs.ml +++ b/infer/src/checkers/reachingDefs.ml @@ -59,7 +59,7 @@ end (* initialize formal parameters to have start node as reaching def *) let init_reaching_defs_with_formals pdesc = let start_node_defs = Defs.singleton (Procdesc.get_start_node pdesc) in - BufferOverrunSemantics.get_formals pdesc + BufferOverrunDomain.get_formals pdesc |> List.fold_left ~init:ReachingDefsMap.empty ~f:(fun acc (pvar, _) -> ReachingDefsMap.add (Var.of_pvar pvar) start_node_defs acc )