diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index cac88ad7f..c8bf45e83 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -95,11 +95,11 @@ module TransferFunctions = struct in let ret_var = Loc.of_var (Var.of_id ret_id) in let ret_val = - let val_of_return_var = - Dom.Mem.find_opt (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem - in - IOption.value_default_f val_of_return_var ~f:(fun () -> - Dom.Val.of_loc (Loc.of_pvar (Pvar.get_ret_param_pvar callee_pname)) ) + match Procdesc.load callee_pname with + | Some callee_pdesc when Procdesc.has_added_return_param callee_pdesc -> + Dom.Val.of_loc (Loc.of_pvar (Pvar.get_ret_param_pvar callee_pname)) + | _ -> + Dom.Mem.find (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem in Dom.Mem.add_stack ret_var (Dom.Val.subst ret_val eval_sym_trace location) mem |> instantiate_ret_alias