diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index f6abe0dd3..7825cebff 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -41,10 +41,14 @@ let should_report_on_type t = false +type extras = {formals: FormalMap.t; summary: Summary.t} + module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = RecordDomain + type nonrec extras = extras + let report_intra access_expr loc summary = let message = F.asprintf "The value read from %a was never initialized" AccessExpression.pp access_expr @@ -53,8 +57,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Reporting.log_error summary ~loc ~ltr IssueType.uninitialized_value message - type extras = FormalMap.t * Summary.t - let is_struct t = match t.Typ.desc with Typ.Tstruct _ -> true | _ -> false let is_array t = match t.Typ.desc with Typ.Tarray _ -> true | _ -> false @@ -104,7 +106,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct || is_array_element_passed_by_ref call t access_expr idx - let report_on_function_params pdesc tenv uninit_vars actuals loc extras call = + let report_on_function_params pdesc tenv uninit_vars actuals loc summary call = List.iteri ~f:(fun idx e -> match e with @@ -114,7 +116,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct should_report_var pdesc tenv uninit_vars access_expr && (not (Typ.is_pointer t)) && not (is_struct_field_passed_by_ref call t access_expr idx) - then report_intra access_expr loc (snd extras) + then report_intra access_expr loc summary else () | _ -> () ) @@ -240,12 +242,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct false - let exec_instr (astate : Domain.astate) {ProcData.pdesc; ProcData.extras; ProcData.tenv} _ + let exec_instr (astate : Domain.astate) {ProcData.pdesc; extras= {formals; summary}; tenv} _ (instr : HilInstr.t) = let update_prepost access_expr rhs = let lhs_base = AccessExpression.get_base access_expr in if - FormalMap.is_formal lhs_base (fst extras) + FormalMap.is_formal lhs_base formals && Typ.is_pointer (snd lhs_base) && ( (not (is_pointer_assignment tenv access_expr rhs)) || not (AccessExpression.is_base access_expr) ) @@ -276,7 +278,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct ( match rhs_expr with | AccessExpression rhs_access_expr -> if should_report_var pdesc tenv uninit_vars rhs_access_expr && is_lhs_not_a_pointer - then report_intra rhs_access_expr loc (snd extras) + then report_intra rhs_access_expr loc summary | _ -> () ) ; {astate with uninit_vars; prepost} @@ -343,14 +345,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct acc ) in Option.value_map ~default:() - ~f:(report_on_function_params pdesc tenv uninit_vars actuals loc extras) + ~f:(report_on_function_params pdesc tenv uninit_vars actuals loc summary) pname_opt ; {astate with uninit_vars} | Assume (expr, _, _, loc) -> ( match expr with | AccessExpression rhs_access_expr -> if should_report_var pdesc tenv astate.uninit_vars rhs_access_expr then - report_intra rhs_access_expr loc (snd extras) + report_intra rhs_access_expr loc summary | _ -> () ) ; astate @@ -395,14 +397,16 @@ end let checker {Callbacks.tenv; summary; proc_desc} : Summary.t = (* start with empty set of uninit local vars and empty set of init formal params *) - let formal_map = FormalMap.make proc_desc in let uninit_vars = Initial.get_locals tenv proc_desc in let initial = { RecordDomain.uninit_vars= UninitVars.of_list uninit_vars ; aliased_vars= AliasedVars.empty ; prepost= {UninitDomain.pre= D.empty; post= D.empty} } in - let proc_data = ProcData.make proc_desc tenv (formal_map, summary) in + let proc_data = + let formals = FormalMap.make proc_desc in + ProcData.make proc_desc tenv {formals; summary} + in match Analyzer.compute_post proc_data ~initial with | Some {RecordDomain.prepost} -> Payload.update_summary prepost summary