[biabduction] catch exceptions more broadly

Summary:
The biabduction backend can raise exceptions that will be caught when triggered
from within the biabduction backend itself (eg, `analyze_procedure` called from
Symexec as a result of an ondemand analysis, because Symexec will catch these),
but not caught when called as the result of an ondemand analysis emanating from
another analyzer (eg ThreadSafety).

Make the biabduction more self-contained by wrapping the analysis of a
procedure inside a `try/with` with similar properties as the one of Symexec.

Reviewed By: jeremydubreil

Differential Revision: D5986335

fbshipit-source-id: 36a5d32
master
Jules Villard 7 years ago committed by Facebook Github Bot
parent 810d756f79
commit da8333718a

@ -933,8 +933,7 @@ let perform_analysis_phase tenv (summary: Specs.summary) (proc_cfg: ProcCfg.Exce
Exceptions.Internal_error
(Localise.verbatim_desc "Leak_while_collecting_specs_after_footprint")
in
Reporting.log_error_deprecated pname exn ; []
(* retuning no specs *)
Reporting.log_error_deprecated pname exn ; (* retuning no specs *) []
in
(specs, Specs.FOOTPRINT)
in
@ -1317,7 +1316,10 @@ let analyze_procedure_aux cg_opt tenv proc_desc =
let analyze_procedure {Callbacks.summary; proc_desc; tenv} : Specs.summary =
let proc_name = Procdesc.get_proc_name proc_desc in
Specs.add_summary proc_name summary ;
ignore (analyze_procedure_aux None tenv proc_desc) ;
( try ignore (analyze_procedure_aux None tenv proc_desc)
with exn ->
reraise_if exn ~f:(fun () -> not (Exceptions.handle_exception exn)) ;
Reporting.log_error_deprecated proc_name exn ) ;
Specs.get_summary_unsafe __FILE__ proc_name
(** Create closures to perform the analysis of an exe_env *)

@ -172,9 +172,8 @@ let analyze_proc_desc curr_pdesc callee_pdesc : Specs.summary option =
Some (run_proc_analysis callbacks.analyze_ondemand curr_pdesc callee_pdesc)
else Specs.get_summary callee_pname
(** analyze_proc_name curr_pdesc proc_name
performs an on-demand analysis of proc_name
triggered during the analysis of curr_pname. *)
(** analyze_proc_name curr_pdesc proc_name performs an on-demand analysis of proc_name triggered
during the analysis of curr_pname *)
let analyze_proc_name curr_pdesc callee_pname : Specs.summary option =
match !callbacks_ref with
| None

Loading…
Cancel
Save