@ -433,13 +433,21 @@ module DisjunctiveAnalyzer =
let widen_policy = ` UnderApproximateAfterNumIterations Config . pulse_widen_threshold
let widen_policy = ` UnderApproximateAfterNumIterations Config . pulse_widen_threshold
end )
end )
let with_debug_exit_node proc_desc ~ f =
AnalysisCallbacks . html_debug_new_node_session
( Procdesc . get_exit_node proc_desc )
~ pp_name : ( fun fmt -> F . pp_print_string fmt " pulse summary creation " )
~ f
let checker ( { InterproceduralAnalysis . proc_desc ; err_log } as analysis_data ) =
let checker ( { InterproceduralAnalysis . proc_desc ; err_log } as analysis_data ) =
AbstractValue . State . reset () ;
AbstractValue . State . reset () ;
let initial = [ ExecutionDomain . mk_initial proc_desc ] in
let initial = [ ExecutionDomain . mk_initial proc_desc ] in
match DisjunctiveAnalyzer . compute_post analysis_data ~ initial proc_desc with
match DisjunctiveAnalyzer . compute_post analysis_data ~ initial proc_desc with
| Some posts ->
| Some posts ->
let summary = PulseSummary . of_posts proc_desc posts in
with_debug_exit_node proc_desc ~ f : ( fun () ->
report_topl_errors proc_desc err_log summary ;
let summary = PulseSummary . of_posts proc_desc posts in
Some summary
report_topl_errors proc_desc err_log summary ;
Some summary )
| None ->
| None ->
None
None