[biabduction] more exception auditing

Summary: The `Utils` module has another version of try-finally than can swallow exceptions from the restart scheduler. This diff fixes that, but has to also fix the dependency cycle introduced between `SymOp` and `Utils`. This is done by extracting the exception handling from `SymOp` into a new base module `Exception`.

Reviewed By: jvillard

Differential Revision: D28930082

fbshipit-source-id: 7894d8c89

infer/src/absint/InterproceduralAnalysis.ml

@@ -13,7 +13,7 @@ type 'payload t =
   ; err_log: Errlog.t
   ; exe_env: Exe_env.t
   ; analyze_dependency: Procname.t -> (Procdesc.t * 'payload) option
-  ; update_stats: ?add_symops:int -> ?failure_kind:SymOp.failure_kind -> unit -> unit }
+  ; update_stats: ?add_symops:int -> ?failure_kind:Exception.failure_kind -> unit -> unit }
 
 type 'payload file_t =
   { source_file: SourceFile.t

infer/src/absint/InterproceduralAnalysis.mli

@@ -20,7 +20,7 @@ type 'payload t =
   ; analyze_dependency: Procname.t -> (Procdesc.t * 'payload) option
         (** On-demand analysis of callees or other dependencies of the analysis of the current
             procedure. Uses [Ondemand.analyze_procedure]. *)
-  ; update_stats: ?add_symops:int -> ?failure_kind:SymOp.failure_kind -> unit -> unit
+  ; update_stats: ?add_symops:int -> ?failure_kind:Exception.failure_kind -> unit -> unit
         (** update the [Summary.Stats.t] of the summary of the current procedure *) }
 
 (** Analysis data for the analysis of a source file. *)

infer/src/backend/NodePrinter.ml

@@ -44,5 +44,5 @@ let with_session ?kind ~pp_name node ~f =
     AnalysisState.set_session session ;
     let pp_name = Option.fold kind ~init:pp_name ~f:with_kind in
     Printer.node_start_session ~pp_name node session ;
-    SymOp.try_finally ~f ~finally:(fun () -> Printer.node_finish_session node) )
+    Exception.try_finally ~f ~finally:(fun () -> Printer.node_finish_session node) )
   else f ()

infer/src/backend/Summary.ml

@@ -12,7 +12,7 @@ module L = Logging
 
 module Stats = struct
   type t =
-    { failure_kind: SymOp.failure_kind option
+    { failure_kind: Exception.failure_kind option
           (** what type of failure stopped the analysis (if any) *)
     ; symops: int  (** Number of SymOp's throughout the whole analysis of the function *)
     ; mutable nodes_visited: IntSet.t  (** Nodes visited *) }
@@ -32,7 +32,7 @@ module Stats = struct
   let pp_failure_kind_opt fmt failure_kind_opt =
     match failure_kind_opt with
     | Some failure_kind ->
-        SymOp.pp_failure_kind fmt failure_kind
+        Exception.pp_failure_kind fmt failure_kind
     | None ->
         F.pp_print_string fmt "NONE"
 

infer/src/backend/Summary.mli

@@ -19,7 +19,7 @@ module Stats : sig
 
   val is_visited : t -> int -> bool
 
-  val update : ?add_symops:int -> ?failure_kind:SymOp.failure_kind -> t -> t
+  val update : ?add_symops:int -> ?failure_kind:Exception.failure_kind -> t -> t
 end
 
 module Status : sig

infer/src/backend/ondemand.ml

@@ -237,7 +237,7 @@ let run_proc_analysis exe_env ~caller_pdesc callee_pdesc =
     L.internal_error "@\nERROR RUNNING BACKEND: %a %s@\n@\nBACK TRACE@\n%s@?" Procname.pp
       callee_pname (Exn.to_string exn) backtrace ;
     match exn with
-    | SymOp.Analysis_failure_exe kind ->
+    | Exception.Analysis_failure_exe kind ->
         (* in production mode, log the timeout/crash and continue with the summary we had before
            the failure occurred *)
         log_error_and_continue exn initial_callee_summary kind

infer/src/base/DBWriter.ml

@@ -373,7 +373,7 @@ module Server = struct
           Unix.close socket ;
           Unix.remove socket_name )
     in
-    Utils.try_finally_swallow_timeout ~f:(fun () -> server_loop socket) ~finally:shutdown
+    Exception.try_finally ~f:(fun () -> server_loop socket) ~finally:shutdown
 
 
   let send cmd =

infer/src/base/Exception.ml

@@ -0,0 +1,57 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+module F = Format
+
+type failure_kind =
+  | FKtimeout  (** max time exceeded *)
+  | FKsymops_timeout of int  (** max symop's exceeded *)
+  | FKrecursion_timeout of int  (** max recursion level exceeded *)
+  | FKcrash of string  (** uncaught exception or failed assertion *)
+
+(** failure that prevented biabduction analysis from finishing *)
+exception Analysis_failure_exe of failure_kind
+
+let exn_not_failure = function
+  | Analysis_failure_exe _ | RestartSchedulerException.ProcnameAlreadyLocked _ ->
+      false
+  | _ ->
+      true
+
+
+let try_finally ~f ~finally =
+  match f () with
+  | r ->
+      finally () ;
+      r
+  | exception (Analysis_failure_exe _ as f_exn) ->
+      IExn.reraise_after f_exn ~f:(fun () ->
+          try finally ()
+          with finally_exn when RestartSchedulerException.is_not_restart_exception finally_exn ->
+            (* swallow in favor of the original exception unless it's the restart scheduler exception *)
+            () )
+  | exception f_exn when RestartSchedulerException.is_not_restart_exception f_exn ->
+      IExn.reraise_after f_exn ~f:(fun () ->
+          try finally ()
+          with
+          | finally_exn
+          when (* do not swallow Analysis_failure_exe or restart exception thrown from finally *)
+               exn_not_failure finally_exn
+          ->
+            () )
+
+
+let pp_failure_kind fmt = function
+  | FKtimeout ->
+      F.pp_print_string fmt "TIMEOUT"
+  | FKsymops_timeout symops ->
+      F.fprintf fmt "SYMOPS TIMEOUT (%d)" symops
+  | FKrecursion_timeout level ->
+      F.fprintf fmt "RECURSION TIMEOUT (%d)" level
+  | FKcrash msg ->
+      F.fprintf fmt "CRASH (%s)" msg

infer/src/base/Exception.mli

@@ -0,0 +1,30 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** The restart scheduler and biabduction use exceptions for control flow (restarts/timeouts
+    respectively). Functions here abstract away the semantics of when an exception can be ignored. *)
+
+open! IStd
+
+(** types of biabduction failure due to timeouts *)
+type failure_kind =
+  | FKtimeout  (** max time exceeded *)
+  | FKsymops_timeout of int  (** max symop's exceeded *)
+  | FKrecursion_timeout of int  (** max recursion level exceeded *)
+  | FKcrash of string  (** uncaught exception or failed assertion *)
+
+val pp_failure_kind : Format.formatter -> failure_kind -> unit
+
+(** Timeout exception *)
+exception Analysis_failure_exe of failure_kind
+
+val exn_not_failure : exn -> bool
+(** check that the exception is not a biabduction timeout or restart scheduler exception *)
+
+val try_finally : f:(unit -> 'a) -> finally:(unit -> unit) -> 'a
+(** [try_finally ~f ~finally] executes [f] and then [finally] even if [f] raises an exception.
+    Biabduction timeouts and restart scheduler exceptions are handled as necessary. *)

infer/src/base/SymOp.ml

@@ -9,56 +9,6 @@
 (** Symbolic Operations and Failures: the units in which analysis work is measured *)
 
 open! IStd
-module F = Format
-
-type failure_kind =
-  | FKtimeout  (** max time exceeded *)
-  | FKsymops_timeout of int  (** max symop's exceeded *)
-  | FKrecursion_timeout of int  (** max recursion level exceeded *)
-  | FKcrash of string  (** uncaught exception or failed assertion *)
-
-(** failure that prevented analysis from finishing *)
-exception Analysis_failure_exe of failure_kind
-
-let exn_not_failure = function
-  | Analysis_failure_exe _ | RestartSchedulerException.ProcnameAlreadyLocked _ ->
-      false
-  | _ ->
-      true
-
-
-let try_finally ~f ~finally =
-  match f () with
-  | r ->
-      finally () ;
-      r
-  | exception (Analysis_failure_exe _ as f_exn) ->
-      IExn.reraise_after f_exn ~f:(fun () ->
-          try finally ()
-          with finally_exn when RestartSchedulerException.is_not_restart_exception finally_exn ->
-            (* swallow in favor of the original exception unless it's the restart scheduler exception *)
-            () )
-  | exception f_exn when RestartSchedulerException.is_not_restart_exception f_exn ->
-      IExn.reraise_after f_exn ~f:(fun () ->
-          try finally ()
-          with
-          | finally_exn
-          when (* do not swallow Analysis_failure_exe thrown from finally *)
-               exn_not_failure finally_exn
-          ->
-            () )
-
-
-let pp_failure_kind fmt = function
-  | FKtimeout ->
-      F.pp_print_string fmt "TIMEOUT"
-  | FKsymops_timeout symops ->
-      F.fprintf fmt "SYMOPS TIMEOUT (%d)" symops
-  | FKrecursion_timeout level ->
-      F.fprintf fmt "RECURSION TIMEOUT (%d)" level
-  | FKcrash msg ->
-      F.fprintf fmt "CRASH (%s)" msg
-
 
 (** Count the number of symbolic operations *)
 
@@ -151,7 +101,7 @@ let pay () =
   !gs.symop_total := !(!gs.symop_total) + 1 ;
   ( match !timeout_symops with
   | Some symops when !gs.symop_count > symops && !gs.alarm_active ->
-      raise (Analysis_failure_exe (FKsymops_timeout !gs.symop_count))
+      raise (Exception.Analysis_failure_exe (FKsymops_timeout !gs.symop_count))
   | _ ->
       () ) ;
   check_wallclock_alarm ()

infer/src/base/SymOp.mli

@@ -52,23 +52,3 @@ val unset_alarm : unit -> unit
 
 val unset_wallclock_alarm : unit -> unit
 (** Unset the wallclock alarm checked at every pay() *)
-
-type failure_kind =
-  | FKtimeout  (** max time exceeded *)
-  | FKsymops_timeout of int  (** max symop's exceeded *)
-  | FKrecursion_timeout of int  (** max recursion level exceeded *)
-  | FKcrash of string  (** uncaught exception or failed assertion *)
-
-(** Timeout exception *)
-exception Analysis_failure_exe of failure_kind
-
-val exn_not_failure : exn -> bool
-(** check that the exception is not a timeout exception *)
-
-val try_finally : f:(unit -> 'a) -> finally:(unit -> unit) -> 'a
-(** [try_finally ~f ~finally] executes [f] and then [finally] even if [f] raises an exception.
-    Assuming that [finally ()] terminates quickly [Analysis_failure_exe] exceptions are handled
-    correctly. In particular, an exception raised by [f ()] is delayed until [finally ()] finishes,
-    so [finally ()] should return reasonably quickly. *)
-
-val pp_failure_kind : Format.formatter -> failure_kind -> unit

infer/src/base/Utils.ml

@@ -215,33 +215,24 @@ let read_safe_json_file path =
 
 
 let do_finally_swallow_timeout ~f ~finally =
-  let res =
-    try f ()
-    with exc ->
-      IExn.reraise_after exc ~f:(fun () ->
-          try finally () |> ignore with _ -> (* swallow in favor of the original exception *) () )
-  in
-  let res' = finally () in
-  (res, res')
-
-
-let try_finally_swallow_timeout ~f ~finally =
-  let res, () = do_finally_swallow_timeout ~f ~finally in
-  res
+  let res_finally = ref None in
+  let finally () = res_finally := Some (finally ()) in
+  let res = Exception.try_finally ~f ~finally in
+  (res, Option.value_exn !res_finally)
 
 
 let with_file_in file ~f =
   let ic = In_channel.create file in
   let f () = f ic in
   let finally () = In_channel.close ic in
-  try_finally_swallow_timeout ~f ~finally
+  Exception.try_finally ~f ~finally
 
 
 let with_file_out file ~f =
   let oc = Out_channel.create file in
   let f () = f oc in
   let finally () = Out_channel.close oc in
-  try_finally_swallow_timeout ~f ~finally
+  Exception.try_finally ~f ~finally
 
 
 let with_intermediate_temp_file_out file ~f =
@@ -251,7 +242,7 @@ let with_intermediate_temp_file_out file ~f =
     Out_channel.close temp_oc ;
     Unix.rename ~src:temp_filename ~dst:file
   in
-  try_finally_swallow_timeout ~f ~finally
+  Exception.try_finally ~f ~finally
 
 
 let write_json_to_file destfile json =
@@ -438,7 +429,7 @@ let timeit ~f =
 let do_in_dir ~dir ~f =
   let cwd = Unix.getcwd () in
   Unix.chdir dir ;
-  try_finally_swallow_timeout ~f ~finally:(fun () -> Unix.chdir cwd)
+  Exception.try_finally ~f ~finally:(fun () -> Unix.chdir cwd)
 
 
 let get_available_memory_MB () =

infer/src/base/Utils.mli

@@ -102,10 +102,6 @@ val suppress_stderr2 : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c
 val rmtree : string -> unit
 (** [rmtree path] removes [path] and, if [path] is a directory, recursively removes its contents *)
 
-val try_finally_swallow_timeout : f:(unit -> 'a) -> finally:(unit -> unit) -> 'a
-(** Calls [f] then [finally] even if [f] raised an exception. The original exception is reraised
-    afterwards. Where possible use [SymOp.try_finally] to avoid swallowing timeouts. *)
-
 val better_hash : 'a -> Caml.Digest.t
 (** Hashtbl.hash only hashes the first 10 meaningful values, [better_hash] uses everything. *)
 

infer/src/biabduction/BiabductionConfig.ml

@@ -13,7 +13,7 @@ open! IStd
 let set_reference_and_call_function reference value f x =
   let saved = !reference in
   let restore () = reference := saved in
-  Utils.try_finally_swallow_timeout
+  Exception.try_finally
     ~f:(fun () ->
       reference := value ;
       f x )

infer/src/biabduction/Dom.ml

@@ -1717,7 +1717,7 @@ let sigma_partial_join tenv mode (sigma1 : Prop.sigma) (sigma2 : Prop.sigma) :
   CheckJoin.init mode sigma1 sigma2 ;
   let lost_little = CheckJoin.lost_little in
   let s1, s2, s3 = sigma_partial_join' tenv mode [] sigma1 sigma2 in
-  SymOp.try_finally
+  Exception.try_finally
     ~f:(fun () ->
       if Rename.check lost_little then (s1, s2, s3)
       else (
@@ -1996,7 +1996,7 @@ let prop_partial_meet tenv p1 p2 =
   FreshVarExp.init () ;
   Todo.init () ;
   try
-    SymOp.try_finally
+    Exception.try_finally
       ~f:(fun () -> Some (eprop_partial_meet tenv p1 p2))
       ~finally:(fun () ->
         Rename.final () ;
@@ -2110,7 +2110,7 @@ let prop_partial_join ({InterproceduralAnalysis.tenv; _} as analysis_data) mode
       FreshVarExp.init () ;
       Todo.init () ;
       try
-        SymOp.try_finally
+        Exception.try_finally
           ~f:(fun () ->
             let p1', p2' = footprint_partial_join' tenv p1 p2 in
             let rename_footprint = Rename.reset () in
@@ -2132,7 +2132,7 @@ let eprop_partial_join tenv mode (ep1 : Prop.exposed Prop.t) (ep2 : Prop.exposed
   Rename.init () ;
   FreshVarExp.init () ;
   Todo.init () ;
-  SymOp.try_finally
+  Exception.try_finally
     ~f:(fun () -> eprop_partial_join' tenv mode ep1 ep2)
     ~finally:(fun () ->
       Rename.final () ;

infer/src/biabduction/DotBiabduction.ml

@@ -1082,4 +1082,4 @@ let pp_speclist_to_file (filename : DB.filename) spec_list =
 
 
 let emit_specs_to_file filename spec_list =
-  try pp_speclist_to_file filename spec_list with exn when SymOp.exn_not_failure exn -> ()
+  try pp_speclist_to_file filename spec_list with exn when Exception.exn_not_failure exn -> ()

infer/src/biabduction/Exceptions.ml

@@ -159,7 +159,7 @@ let recognize_exception exn : IssueToReport.t =
       {issue_type= IssueType.precondition_not_met; description= desc; ocaml_pos= Some ocaml_pos}
   | Retain_cycle (desc, ocaml_pos) ->
       {issue_type= IssueType.retain_cycle; description= desc; ocaml_pos= Some ocaml_pos}
-  | SymOp.Analysis_failure_exe _ ->
+  | Exception.Analysis_failure_exe _ ->
       {issue_type= IssueType.failure_exe; description= Localise.no_desc; ocaml_pos= None}
   | Skip_function desc ->
       {issue_type= IssueType.skip_function; description= desc; ocaml_pos= None}

infer/src/biabduction/Paths.ml

@@ -330,7 +330,7 @@ end = struct
     let path_pos_at_path p =
       try
         match curr_node p with Some node -> Option.is_some pos_opt && filter node | None -> false
-      with exn when SymOp.exn_not_failure exn -> false
+      with exn when Exception.exn_not_failure exn -> false
     in
     let position_seen = ref false in
     let inverse_sequence =

infer/src/biabduction/Prover.ml

@@ -15,7 +15,7 @@ module F = Format
 
 let decrease_indent_when_exception thunk =
   try thunk ()
-  with exn when SymOp.exn_not_failure exn ->
+  with exn when Exception.exn_not_failure exn ->
     IExn.reraise_after exn ~f:(fun () -> L.d_decrease_indent ())
 
 
@@ -2114,7 +2114,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
                   let res =
                     decrease_indent_when_exception (fun () ->
                         try sigma_imply tenv calc_index_frame calc_missing subs prop1 hpred_list2
-                        with exn when SymOp.exn_not_failure exn ->
+                        with exn when Exception.exn_not_failure exn ->
                           L.d_strln ~color:Red "backtracking lseg: trying rhs of length exactly 1" ;
                           let _, para_inst3 = Predicates.hpara_instantiate para2 e2_ f2_ elist2 in
                           sigma_imply tenv calc_index_frame calc_missing subs prop1 para_inst3 )

infer/src/biabduction/State.ml

@@ -179,7 +179,7 @@ let extract_pre p tenv pdesc abstract_fun =
   in
   let _, p' = PropUtil.remove_locals_formals tenv pdesc p in
   let pre, _ = Prop.extract_spec p' in
-  let pre' = try abstract_fun tenv pre with exn when SymOp.exn_not_failure exn -> pre in
+  let pre' = try abstract_fun tenv pre with exn when Exception.exn_not_failure exn -> pre in
   Prop.normalize tenv (Prop.prop_sub sub pre')
 
 

infer/src/biabduction/SymExec.ml

@@ -1360,7 +1360,7 @@ and instrs ?(mask_errors = false) analysis_data instrs ppl =
     L.d_ln () ;
     try sym_exec analysis_data instr p path
     with exn ->
-      IExn.reraise_if exn ~f:(fun () -> (not mask_errors) || not (SymOp.exn_not_failure exn)) ;
+      IExn.reraise_if exn ~f:(fun () -> (not mask_errors) || not (Exception.exn_not_failure exn)) ;
       let error = Exceptions.recognize_exception exn in
       let loc =
         match error.ocaml_pos with
@@ -1585,7 +1585,7 @@ and check_variadic_sentinel ?(fails_on_nil = false) n_formals (sentinel, null_po
     let tmp_id_deref = Ident.create_fresh Ident.kprimed in
     let load_instr = Sil.Load {id= tmp_id_deref; e= lexp; root_typ= typ; typ; loc} in
     try instrs analysis_data (Instrs.singleton load_instr) result
-    with e when SymOp.exn_not_failure e ->
+    with e when Exception.exn_not_failure e ->
       IExn.reraise_if e ~f:(fun () -> fails_on_nil) ;
       let deref_str = Localise.deref_str_nil_argument_in_variadic_method proc_name nargs i in
       let err_desc =

infer/src/biabduction/Tabulation.ml

@@ -473,7 +473,7 @@ let rec fsel_star_fld fsel1 fsel2 =
 
 
 and array_content_star se1 se2 =
-  try sexp_star_fld se1 se2 with exn when SymOp.exn_not_failure exn -> se1
+  try sexp_star_fld se1 se2 with exn when Exception.exn_not_failure exn -> se1
 
 
 (* let postcondition override *)
@@ -581,7 +581,7 @@ let sigma_star_fld tenv (sigma1 : Predicates.hpred list) (sigma2 : Predicates.hp
           star sg1 sigma2' )
   in
   try star sigma1 sigma2
-  with exn when SymOp.exn_not_failure exn ->
+  with exn when Exception.exn_not_failure exn ->
     L.d_str "cannot star " ;
     Prop.d_sigma sigma1 ;
     L.d_str " and " ;
@@ -620,7 +620,7 @@ let sigma_star_typ (sigma1 : Predicates.hpred list) (typings2 : (Exp.t * Exp.t)
           star sg1 typings2' )
   in
   try star sigma1 typings2
-  with exn when SymOp.exn_not_failure exn ->
+  with exn when Exception.exn_not_failure exn ->
     L.d_str "cannot star " ;
     Prop.d_sigma sigma1 ;
     L.d_str " and " ;

infer/src/biabduction/Timeout.ml

@@ -73,7 +73,7 @@ let set_status status =
 
 let timeout_action _ =
   unset_alarm () ;
-  raise (SymOp.Analysis_failure_exe FKtimeout)
+  raise (Exception.Analysis_failure_exe FKtimeout)
 
 
 let register_timeout_handlers =
@@ -120,13 +120,13 @@ let exe_timeout f x =
     SymOp.set_alarm ()
   in
   try
-    SymOp.try_finally
+    Exception.try_finally
       ~f:(fun () ->
         suspend_existing_timeout_and_start_new_one () ;
         f x ;
         None )
       ~finally:resume_previous_timeout
-  with SymOp.Analysis_failure_exe kind ->
+  with Exception.Analysis_failure_exe kind ->
     let loc = AnalysisState.get_loc () |> Option.value ~default:Location.dummy in
-    Errdesc.warning_err loc "TIMEOUT: %a@." SymOp.pp_failure_kind kind ;
+    Errdesc.warning_err loc "TIMEOUT: %a@." Exception.pp_failure_kind kind ;
     Some kind

infer/src/biabduction/Timeout.mli

@@ -9,7 +9,7 @@ open! IStd
 
 (** Handle timeout events *)
 
-val exe_timeout : ('a -> unit) -> 'a -> SymOp.failure_kind option
+val exe_timeout : ('a -> unit) -> 'a -> Exception.failure_kind option
 (** Execute the function up to a given timeout. *)
 
 val resume_previous_timeout : unit -> unit

infer/src/biabduction/errdesc.ml

@@ -992,7 +992,7 @@ let explain_nth_function_parameter proc_name tenv use_buckets deref_str prop n p
         match dexp_opt with Some de -> Some (dexp_apply_pvar_off de pvar_off) | None -> None
       in
       create_dereference_desc proc_name tenv ~use_buckets dexp_opt' deref_str prop loc
-    with exn when SymOp.exn_not_failure exn -> Localise.no_desc )
+    with exn when Exception.exn_not_failure exn -> Localise.no_desc )
   | _ ->
       Localise.no_desc
 

infer/src/biabduction/interproc.ml

@@ -1045,7 +1045,7 @@ let perform_transition ({InterproceduralAnalysis.tenv; _} as analysis_data) proc
         match ProcCfg.Exceptional.start_node proc_cfg with
         | start_node ->
             AnalysisCallbacks.html_debug_new_node_session ~pp_name start_node ~f
-        | exception exn when SymOp.exn_not_failure exn ->
+        | exception exn when Exception.exn_not_failure exn ->
             f ()
       in
       with_start_node_session ~f:(fun () ->
@@ -1054,7 +1054,7 @@ let perform_transition ({InterproceduralAnalysis.tenv; _} as analysis_data) proc
             let res = collect_preconditions analysis_data summary in
             BiabductionConfig.allow_leak := allow_leak ;
             res
-          with exn when SymOp.exn_not_failure exn ->
+          with exn when Exception.exn_not_failure exn ->
             BiabductionConfig.allow_leak := allow_leak ;
             L.debug Analysis Medium "Error in collect_preconditions for %a@." Procname.pp proc_name ;
             let error = Exceptions.recognize_exception exn in