diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index aa77b2c69..78efc825e 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -448,9 +448,16 @@ let set_attributes pdesc attributes = pdesc.attributes <- attributes let get_exit_node pdesc = pdesc.exit_node +let get_proc_name pdesc = pdesc.attributes.proc_name + (** Return name and type of formal parameters *) let get_formals pdesc = pdesc.attributes.formals +let get_pvar_formals pdesc = + let proc_name = get_proc_name pdesc in + get_formals pdesc |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ)) + + let get_loc pdesc = pdesc.attributes.loc (** Return name and type of local variables *) @@ -468,8 +475,6 @@ let get_nodes pdesc = pdesc.nodes let get_nodes_num pdesc = pdesc.nodes_num -let get_proc_name pdesc = pdesc.attributes.proc_name - (** Return the return type of the procedure *) let get_ret_type pdesc = pdesc.attributes.ret_type diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index 1111bea87..3a8228acf 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -219,6 +219,9 @@ val get_exit_node : t -> Node.t val get_formals : t -> (Mangled.t * Typ.t) list (** Return name and type of formal parameters *) +val get_pvar_formals : t -> (Pvar.t * Typ.t) list +(** Return pvar and type of formal parameters *) + val get_loc : t -> Location.t (** Return loc information for the procedure *) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 501748a04..5fcb4faa0 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -75,7 +75,7 @@ module TransferFunctions = struct let instantiate_mem_reachable (ret_id, _) callee_pdesc callee_pname ~callee_exit_mem ({Dom.eval_locpath} as eval_sym_trace) mem location = - let formals = Dom.get_formals callee_pdesc in + let formals = Procdesc.get_pvar_formals callee_pdesc in let copy_reachable_locs_from locs mem = let copy loc acc = Option.value_map (Dom.Mem.find_opt loc callee_exit_mem) ~default:acc ~f:(fun v -> @@ -207,7 +207,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 Dom.get_formals pdesc with + match Procdesc.get_pvar_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 c420257c8..99528e9c4 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -22,13 +22,9 @@ 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 OndemandEnv = struct + module FormalTyps = Caml.Map.Make (Pvar) + type t = { typ_of_param_path: SPath.partial -> Typ.t option ; may_last_field: SPath.partial -> bool @@ -36,10 +32,9 @@ module OndemandEnv = struct ; integer_type_widths: Typ.IntegerWidths.t } let mk pdesc = - let module FormalTyps = Caml.Map.Make (Pvar) in let formal_typs = - List.fold (get_formals pdesc) ~init:FormalTyps.empty ~f:(fun acc (formal, typ) -> - FormalTyps.add formal typ acc ) + List.fold (Procdesc.get_pvar_formals pdesc) ~init:FormalTyps.empty + ~f:(fun acc (formal, typ) -> FormalTyps.add formal typ acc ) in fun tenv integer_type_widths -> let rec typ_of_param_path = function diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 8686c127f..cf1be2000 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -393,7 +393,7 @@ let eval_sympath params sympath mem = let mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem = let params = - let formals = get_formals callee_pdesc in + let formals = Procdesc.get_pvar_formals callee_pdesc in let actuals = List.map ~f:(fun (a, _) -> eval integer_type_widths a caller_mem) actual_exps in ParamBindings.make formals actuals in @@ -710,7 +710,7 @@ let get_subst_map : in List.rev_append new_rel_matching rel_l in - let formals = get_formals callee_pdesc in + let formals = Procdesc.get_pvar_formals callee_pdesc in let actuals = List.map ~f:(fun (a, _) -> (eval integer_type_widths a caller_mem, Some a)) params in diff --git a/infer/src/checkers/reachingDefs.ml b/infer/src/checkers/reachingDefs.ml index d07733c7a..406f151a8 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 - BufferOverrunDomain.get_formals pdesc + Procdesc.get_pvar_formals pdesc |> List.fold_left ~init:ReachingDefsMap.empty ~f:(fun acc (pvar, _) -> ReachingDefsMap.add (Var.of_pvar pvar) start_node_defs acc )