|
|
|
@ -54,14 +54,9 @@ let check_block_retain_cycle tenv caller_pname prop block_nullified =
|
|
|
|
|
let mblock = Sil.pvar_get_name block_nullified in
|
|
|
|
|
let block_pname = Procname.mangled_objc_block (Mangled.to_string mblock) in
|
|
|
|
|
let block_captured =
|
|
|
|
|
let block_pdesc_opt = match Ondemand.get_cfg caller_pname with
|
|
|
|
|
| Some caller_cfg ->
|
|
|
|
|
Cfg.Procdesc.find_from_name caller_cfg block_pname
|
|
|
|
|
| None ->
|
|
|
|
|
None in
|
|
|
|
|
match block_pdesc_opt with
|
|
|
|
|
| Some block_pdesc ->
|
|
|
|
|
fst (IList.split (Cfg.Procdesc.get_captured block_pdesc))
|
|
|
|
|
match AttributesTable.load_attributes block_pname with
|
|
|
|
|
| Some attributes ->
|
|
|
|
|
fst (IList.split attributes.ProcAttributes.captured)
|
|
|
|
|
| None ->
|
|
|
|
|
[] in
|
|
|
|
|
let prop' = Cfg.remove_seed_captured_vars_block block_captured prop in
|
|
|
|
@ -715,24 +710,30 @@ let resolve_java_pname tenv prop args pname call_flags : Procname.t =
|
|
|
|
|
(** Resolve the procedure name and run the analysis of the resolved procedure
|
|
|
|
|
if not already analyzed *)
|
|
|
|
|
let resolve_and_analyze
|
|
|
|
|
tenv caller_pdesc prop args callee_pname call_flags : Procname.t * Specs.summary option =
|
|
|
|
|
tenv caller_pdesc prop args callee_proc_name call_flags : Procname.t * Specs.summary option =
|
|
|
|
|
(* TODO (#9333890): Fix conflict with method overloading by encoding in the procedure name
|
|
|
|
|
whether the method is defined or generated by the specialization *)
|
|
|
|
|
let analyze_ondemand caller_cfg resolved_pname : unit =
|
|
|
|
|
if Procname.equal resolved_pname callee_pname then
|
|
|
|
|
Ondemand.analyze_proc_name ~propagate_exceptions:true caller_pdesc callee_pname
|
|
|
|
|
let analyze_ondemand resolved_pname : unit =
|
|
|
|
|
if Procname.equal resolved_pname callee_proc_name then
|
|
|
|
|
Ondemand.analyze_proc_name ~propagate_exceptions:true caller_pdesc callee_proc_name
|
|
|
|
|
else
|
|
|
|
|
(* Create the type sprecialized procedure description and analyze it directly *)
|
|
|
|
|
Option.may
|
|
|
|
|
(fun specialized_pdesc ->
|
|
|
|
|
Ondemand.analyze_proc_desc ~propagate_exceptions:true caller_pdesc specialized_pdesc)
|
|
|
|
|
(Cfg.specialize_types caller_cfg callee_pname resolved_pname args) in
|
|
|
|
|
(match Ondemand.get_proc_desc resolved_pname with
|
|
|
|
|
| Some resolved_proc_desc ->
|
|
|
|
|
Some resolved_proc_desc
|
|
|
|
|
| None ->
|
|
|
|
|
begin
|
|
|
|
|
Option.map
|
|
|
|
|
(fun callee_proc_desc ->
|
|
|
|
|
Cfg.specialize_types callee_proc_desc resolved_pname args)
|
|
|
|
|
(Ondemand.get_proc_desc callee_proc_name)
|
|
|
|
|
end) in
|
|
|
|
|
let resolved_pname =
|
|
|
|
|
resolve_java_pname tenv prop args callee_pname call_flags in
|
|
|
|
|
Option.may
|
|
|
|
|
(fun caller_cfg ->
|
|
|
|
|
analyze_ondemand caller_cfg resolved_pname)
|
|
|
|
|
(Ondemand.get_cfg (Cfg.Procdesc.get_proc_name caller_pdesc));
|
|
|
|
|
resolve_java_pname tenv prop args callee_proc_name call_flags in
|
|
|
|
|
analyze_ondemand resolved_pname;
|
|
|
|
|
resolved_pname, Specs.get_summary resolved_pname
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@ -1137,12 +1138,7 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path
|
|
|
|
|
|
|
|
|
|
Ondemand.analyze_proc_name ~propagate_exceptions:true pdesc resolved_pname;
|
|
|
|
|
|
|
|
|
|
let callee_pdesc_opt =
|
|
|
|
|
match Ondemand.get_cfg pname with
|
|
|
|
|
| Some caller_cfg ->
|
|
|
|
|
Cfg.Procdesc.find_from_name caller_cfg resolved_pname
|
|
|
|
|
| None ->
|
|
|
|
|
None in
|
|
|
|
|
let callee_pdesc_opt = Ondemand.get_proc_desc resolved_pname in
|
|
|
|
|
|
|
|
|
|
let ret_typ_opt = Option.map Cfg.Procdesc.get_ret_type callee_pdesc_opt in
|
|
|
|
|
let sentinel_result =
|
|
|
|
|