[attrs] look at capture DB only -- inferbo

Summary:
This call back introduces non-determinism because it first looks for the proc desc in a summary and if it doesn't find it then returns the one from the capture DB.

The problem is:
- the main factor affecting the existence of a summary on-disk is timing;
- the two proc descs are generally different, as the one in the summary is preanalysed and the one in the capture DB is not;
- this extends to the attributes included in the proc desc potentially.

The plan is to eliminate these calls one by one using the CI for correctness.

Reviewed By: skcho

Differential Revision: D29792757

fbshipit-source-id: 744472950
master
Nikos Gorogiannis 4 years ago committed by Facebook GitHub Bot
parent e3685a8d9d
commit aa85648512

@ -474,9 +474,7 @@ let compute_invariant_map :
let proc_name = Procdesc.get_proc_name proc_desc in
let open IOption.Let_syntax in
let get_summary proc_name = analyze_dependency proc_name >>| snd in
let get_formals callee_pname =
AnalysisCallbacks.proc_resolve_attributes callee_pname >>| Pvar.get_pvar_formals
in
let get_formals callee_pname = Attributes.load callee_pname >>| Pvar.get_pvar_formals in
let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in
let oenv = OndemandEnv.mk proc_desc tenv integer_type_widths in
{interproc; get_summary; get_formals; oenv}

@ -457,9 +457,7 @@ let checker ({InterproceduralAnalysis.proc_desc; tenv; exe_env; analyze_dependen
let* _checker_summary, analysis_summary = get_summary_common callee_pname in
analysis_summary
in
let get_formals callee_pname =
AnalysisCallbacks.proc_resolve_attributes callee_pname >>| Pvar.get_pvar_formals
in
let get_formals callee_pname = Attributes.load callee_pname >>| Pvar.get_pvar_formals in
compute_checks get_checks_summary get_summary get_formals proc_name tenv integer_type_widths
cfg inv_map
in

Loading…
Cancel
Save