|
|
@ -95,11 +95,11 @@ module TransferFunctions = struct
|
|
|
|
in
|
|
|
|
in
|
|
|
|
let ret_var = Loc.of_var (Var.of_id ret_id) in
|
|
|
|
let ret_var = Loc.of_var (Var.of_id ret_id) in
|
|
|
|
let ret_val =
|
|
|
|
let ret_val =
|
|
|
|
let val_of_return_var =
|
|
|
|
match Procdesc.load callee_pname with
|
|
|
|
Dom.Mem.find_opt (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem
|
|
|
|
| Some callee_pdesc when Procdesc.has_added_return_param callee_pdesc ->
|
|
|
|
in
|
|
|
|
Dom.Val.of_loc (Loc.of_pvar (Pvar.get_ret_param_pvar callee_pname))
|
|
|
|
IOption.value_default_f val_of_return_var ~f:(fun () ->
|
|
|
|
| _ ->
|
|
|
|
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
|
|
|
|
in
|
|
|
|
Dom.Mem.add_stack ret_var (Dom.Val.subst ret_val eval_sym_trace location) mem
|
|
|
|
Dom.Mem.add_stack ret_var (Dom.Val.subst ret_val eval_sym_trace location) mem
|
|
|
|
|> instantiate_ret_alias
|
|
|
|
|> instantiate_ret_alias
|
|
|
|