distinguishing between failures and timeouts

Summary: public Crashes during the analysis are classified as timeouts in the .specs file. In addition, when there is a timeout, it does not say *why* the timeout occurred (hard time, symops, or recursion). This diff adds this information to the .specs file and adds a "fail hard" mode where crashes and timeouts will actually stop the analysis in developer mode (but will still be hidden in the normal production mode).

Reviewed By: jeremydubreil

Differential Revision: D2725382

fb-gh-sync-id: b0b4e5e

infer/src/backend/cg.ml

@@ -357,7 +357,7 @@ let store_to_file (filename : DB.filename) (call_graph : t) =
 
 let pp_graph_dotty get_specs (g: t) fmt =
   let nodes_with_calls = get_all_nodes g in
-  let num_specs n = try IList.length (get_specs n) with exn when exn_not_timeout exn -> - 1 in
+  let num_specs n = try IList.length (get_specs n) with exn when exn_not_failure exn -> - 1 in
   let get_color (n, calls) =
     if num_specs n != 0 then "green" else "red" in
   let get_shape (n, calls) =

infer/src/backend/dotty.ml

@@ -559,7 +559,7 @@ let rec dotty_mk_set_links dotnodes sigma p f cycle =
            let nodes_e = select_nodes_exp_lambda dotnodes e lambda in
            let address_struct_id =
              try get_coordinate_id (IList.hd (IList.filter (is_source_node_of_exp e) nodes_e))
-             with exn when exn_not_timeout exn -> (* L.out "@\n@\n PROBLEMS!!!!!!!!!!@.@.@."; *) assert false in
+             with exn when exn_not_failure exn -> assert false in
            (* we need to exclude the address node from the sorce of fields. no fields should start from there*)
            let nl'= IList.filter (fun id -> address_struct_id != id) nl in
            let links_from_fields = IList.flatten (IList.map ff nl') in
@@ -923,7 +923,7 @@ let pp_dotty_prop_list_in_path f plist prev_n curr_n =
                  pp_dotty f (Generic_proposition) po None) plist;
     if prev_n <> - 1 then F.fprintf f "\n state%iN ->state%iN\n" prev_n curr_n;
     F.fprintf f "\n } \n"
-  with exn when exn_not_timeout exn ->
+  with exn when exn_not_failure exn ->
     ()
 
 (* create a dotty file with a single proposition *)
@@ -937,7 +937,7 @@ let dotty_prop_to_dotty_file fname prop cycle =
     pp_dotty fmt_dot Generic_proposition prop (Some cycle);
     Format.fprintf fmt_dot "@\n}";
     close_out out_dot
-  with exn when exn_not_timeout exn ->
+  with exn when exn_not_failure exn ->
     ()
 
 (* this is used only to print a list of prop parsed with the external parser. Basically deprecated.*)
@@ -954,7 +954,7 @@ let pp_proplist_parsed2dotty_file filename plist =
     let fmt = F.formatter_of_out_channel outc in
     F.fprintf fmt "#### Dotty version:  ####@.%a@.@." pp_list plist;
     close_out outc
-  with exn when exn_not_timeout exn ->
+  with exn when exn_not_failure exn ->
     ()
 
 (********** START of Print interprocedural cfgs in dotty format  *)
@@ -1095,7 +1095,7 @@ let pp_speclist_to_file (filename : DB.filename) spec_list =
 
 let pp_speclist_dotty_file (filename : DB.filename) spec_list =
   try pp_speclist_to_file filename spec_list
-  with exn when exn_not_timeout exn ->
+  with exn when exn_not_failure exn ->
     ()
 
 (**********************************************************************)

infer/src/backend/errdesc.ml

@@ -490,7 +490,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
         (try
            let t2 = Sil.expand_type tenv _t2 in
            Sil.typ_equal t1 t2
-         with exn when exn_not_timeout exn -> false)
+         with exn when exn_not_failure exn -> false)
     | Some (Sil.Sizeof (Sil.Tint _, _)), Some (Sil.Sizeof (Sil.Tint _, _)) when is_file -> (* must be a file opened with "open" *)
         true
     | _ -> false in
@@ -875,7 +875,7 @@ let explain_nth_function_parameter use_buckets deref_str prop n pvar_off =
                Some (dexp_apply_pvar_off de pvar_off)
            | None -> None in
          create_dereference_desc ~use_buckets dexp_opt' deref_str prop loc
-       with exn when exn_not_timeout exn -> Localise.no_desc)
+       with exn when exn_not_failure exn -> Localise.no_desc)
   | _ -> Localise.no_desc
 
 (** Find a program variable whose value is [exp] or pointing to a struct containing [exp] *)

infer/src/backend/exceptions.ml

@@ -198,8 +198,8 @@ let recognize_exception exn =
         (Localise.return_statement_missing, desc, Some mloc, Exn_user, Medium, None, Nocat)
     | Return_value_ignored (desc, mloc) ->
         (Localise.return_value_ignored, desc, Some mloc, Exn_user, Medium, None, Nocat)
-    | Timeout_exe _ ->
+    | Analysis_failure_exe _ ->
-        (Localise.from_string "Timeout_exe", Localise.no_desc, None, Exn_system, Low, None, Nocat)
+        (Localise.from_string "Failure_exe", Localise.no_desc, None, Exn_system, Low, None, Nocat)
     | Skip_function desc ->
         (Localise.skip_function, desc, None, Exn_developer, Low, None, Nocat)
     | Skip_pointer_dereference (desc, mloc) ->

infer/src/backend/fork.ml

@@ -242,7 +242,7 @@ let filter_max exe_env cg filter set priority_set =
 (** Handle timeout events *)
 module Timeout : sig
   (** execute the function up to a given timeout given by the parameter *)
-  val exe_timeout : int -> ('a -> 'b) -> 'a -> 'b option
+  val exe_timeout : int -> ('a -> unit) -> 'a -> failure_kind option
 end = struct
   let set_alarm nsecs =
     match Config.os_type with
@@ -258,17 +258,9 @@ end = struct
     | Config.Unix | Config.Cygwin -> set_alarm 0
     | Config.Win32 -> SymOp.unset_wallclock_alarm ()
 
-  let pp_kind f = function
-    | TOtime ->
-        F.fprintf f "time"
-    | TOrecursion n ->
-        F.fprintf f "recursion %d" n
-    | TOsymops n ->
-        F.fprintf f "SymOps %d" n
-
   let timeout_action _ =
     unset_alarm ();
-    raise (Timeout_exe (TOtime))
+    raise (Analysis_failure_exe (FKtimeout))
 
   let () = begin
     match Config.os_type with
@@ -307,14 +299,14 @@ end = struct
       restore_timeout () in
     try
       before ();
-      let res = f x in
+      f x;
       after ();
-      Some res
+      None
     with
-    | Timeout_exe kind ->
+    | Analysis_failure_exe kind ->
         after ();
-        Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." pp_kind kind;
+        Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." pp_failure_kind kind;
-        None
+        Some kind
     | exe ->
         after ();
         raise exe
@@ -412,21 +404,27 @@ let interprocedural_algorithm
     (_process_result: process_result)
     (filter_out: filter_out) : unit =
   let analyze_proc exe_env pname = (* wrap _analyze_proc and handle exceptions *)
+    let log_error_and_continue exn kind =
+      Reporting.log_error pname exn;
+      let prev_summary = Specs.get_summary_unsafe "interprocedural_algorithm" pname in
+      let timestamp = max 1 (prev_summary.Specs.timestamp) in
+      let stats = { prev_summary.Specs.stats with Specs.stats_failure = Some kind } in
+      let payload =
+        { prev_summary.Specs.payload with Specs.preposts = Some []; } in
+      { prev_summary with Specs.stats; payload; timestamp; } in
+
     try _analyze_proc exe_env pname with
+    | exn when !Config.developer_mode ->
+        (* in developer mode, fail hard on crashes/timeout *)
+        raise exn
+    | Analysis_failure_exe kind as exn ->
+        (* in production mode, log the timeout/crash and continue with the summary we had before
+           the failure occurred *)
+        log_error_and_continue exn kind
     | exn ->
-        Reporting.log_error pname exn;
+        (* this happens due to exceptions from assert false or some other unrecognized exception *)
-        let prev_summary = Specs.get_summary_unsafe "interprocedural_algorithm" pname in
+        log_error_and_continue exn (FKcrash (Printexc.to_string exn)) in
-        let timestamp = max 1 (prev_summary.Specs.timestamp) in
+
-        let stats = { prev_summary.Specs.stats with Specs.stats_timeout = true } in
-        let payload =
-          { prev_summary.Specs.payload with
-            Specs.preposts = Some []; } in
-        let summ =
-          { prev_summary with
-            Specs.stats;
-            payload;
-            timestamp; } in
-        summ in
   let process_result exe_env (pname, calls) summary =
     (* wrap _process_result and handle exceptions *)
     try _process_result exe_env (pname, calls) summary with

infer/src/backend/fork.mli

@@ -13,7 +13,7 @@
 (** Handle timeout events *)
 module Timeout : sig
   (** execute the function up to a given timeout given by the iterations parameter *)
-  val exe_timeout : int -> ('a -> 'b) -> 'a -> 'b option
+  val exe_timeout : int -> ('a -> unit) -> 'a -> Utils.failure_kind option
 end
 
 val this_cluster_files : int ref (** Number of files in the current cluster *)

infer/src/backend/inferprint.ml

@@ -276,12 +276,17 @@ let summary_values top_proc_set summary =
   let call_rank =
     let c1 = 1 and c2 = 1 in
     logscale (c1 * in_calls + c2 * out_calls) in
+
+  let pp_failure failure =
+    pp_to_string pp_failure_kind failure in
+
+
   let cyclomatic = stats.Specs.cyclomatic in
   { vname = Procname.to_string proc_name;
     vname_id = Procname.to_filename proc_name;
     vspecs = IList.length specs;
     vtime = Printf.sprintf "%.0f" stats.Specs.stats_time;
-    vto = if stats.Specs.stats_timeout then "TO" else "  ";
+    vto = Option.map_default pp_failure "NONE" stats.Specs.stats_failure;
     vsymop = stats.Specs.symops;
     verr = Errlog.size
         (fun ekind in_footprint -> ekind = Exceptions.Kerror && in_footprint)
@@ -746,7 +751,9 @@ module Stats = struct
     let is_defective = found_errors in
     let is_verified = specs <> [] && not is_defective in
     let is_checked = not (is_defective || is_verified) in
-    let is_timeout = Specs.(summary.stats.stats_timeout) in
+    let is_timeout = match Specs.(summary.stats.stats_failure) with
+      | None | Some (FKcrash _) -> false
+      | _ -> true in
     stats.nprocs <- stats.nprocs + 1;
     stats.nspecs <- stats.nspecs + (IList.length specs);
     if is_verified then stats.nverified <- stats.nverified + 1;

infer/src/backend/interproc.ml

@@ -900,7 +900,7 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t
     if recursion_level > !Config.max_recursion then
       begin
         L.err "Reached maximum level of recursion, raising a Timeout@.";
-        raise (Timeout_exe (TOrecursion recursion_level))
+        raise (Analysis_failure_exe (FKrecursion_timeout recursion_level))
       end in
 
   let compute_footprint : (unit -> unit) * (unit -> Prop.normal Specs.spec list) =
@@ -1093,12 +1093,14 @@ let update_summary prev_summary specs proc_name elapsed res =
   let timestamp = max 1 (prev_summary.Specs.timestamp + if changed then 1 else 0) in
   let stats_time = prev_summary.Specs.stats.Specs.stats_time +. elapsed in
   let symops = prev_summary.Specs.stats.Specs.symops + SymOp.get_total () in
-  let timeout = res == None || prev_summary.Specs.stats.Specs.stats_timeout in
+  let failure = match res with
+    | None -> prev_summary.Specs.stats.Specs.stats_failure
+    | Some failure_kind -> res in
   let stats =
     { prev_summary.Specs.stats with
       Specs.stats_time = stats_time;
       Specs.symops = symops;
-      Specs.stats_timeout = timeout } in
+      Specs.stats_failure = failure; } in
   let payload =
     { prev_summary.Specs.payload with
       Specs.preposts = Some new_specs; } in
@@ -1148,7 +1150,7 @@ let perform_transition exe_env cg proc_name =
               let start_node = Cfg.Procdesc.get_start_node pdesc in
               f start_node
           | None -> ()
-        with exn when exn_not_timeout exn -> () in
+        with exn when exn_not_failure exn -> () in
       apply_start_node (do_before_node 0);
       try
         Config.allowleak := true;
@@ -1156,7 +1158,7 @@ let perform_transition exe_env cg proc_name =
         Config.allowleak := allowleak;
         apply_start_node do_after_node;
         res
-      with exn when exn_not_timeout exn ->
+      with exn when exn_not_failure exn ->
         apply_start_node do_after_node;
         Config.allowleak := allowleak;
         L.err "Error in collect_preconditions for %a@." Procname.pp proc_name;
@@ -1354,7 +1356,7 @@ let print_stats_cfg proc_shadowed proc_is_active cfg =
         | [], _ -> incr num_nospec_error_proc
         | _, _ -> incr num_spec_error_proc in
       tot_symops := !tot_symops + stats.Specs.symops;
-      if stats.Specs.stats_timeout then incr num_timeout;
+      if Option.is_some stats.Specs.stats_failure then incr num_timeout;
       Errlog.extend_table err_table err_log in
   let print_file_stats fmt () =
     let num_errors = Errlog.err_table_size_footprint Exceptions.Kerror err_table in

infer/src/backend/paths.ml

@@ -311,7 +311,7 @@ end = struct
         | Some node ->
             pos_opt <> None && filter node
         | None -> false
-      with exn when exn_not_timeout exn -> false in
+      with exn when exn_not_failure exn -> false in
     let position_seen = ref false in
     let inverse_sequence =
       let log = ref [] in

infer/src/backend/printer.ml

@@ -351,11 +351,11 @@ end = struct
     try
       Some (Hashtbl.find hash fname)
     with Not_found ->
-      try
+    try
-        let lines_arr = read_file (DB.source_file_to_string fname) in
+      let lines_arr = read_file (DB.source_file_to_string fname) in
-        Hashtbl.add hash fname lines_arr;
+      Hashtbl.add hash fname lines_arr;
-        Some lines_arr
+      Some lines_arr
-      with exn when exn_not_timeout exn -> None
+    with exn when exn_not_failure exn -> None
 
   let from_file_linenum_original hash fname linenum =
     match file_data hash fname with

infer/src/backend/prover.ml

@@ -16,7 +16,7 @@ open Utils
 
 let decrease_indent_when_exception thunk =
   try (thunk ())
-  with exn when exn_not_timeout exn -> (L.d_decrease_indent 1; raise exn)
+  with exn when exn_not_failure exn -> (L.d_decrease_indent 1; raise exn)
 
 let compute_max_from_nonempty_int_list l =
   IList.hd (IList.rev (IList.sort Sil.Int.compare_value l))
@@ -1757,7 +1757,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
                         decrease_indent_when_exception
                           (fun () ->
                              try sigma_imply tenv calc_index_frame calc_missing subs prop1 hpred_list2
-                             with exn when exn_not_timeout exn ->
+                             with exn when exn_not_failure exn ->
                                begin
                                  (L.d_strln_color Red) "backtracking lseg: trying rhs of length exactly 1";
                                  let (_, para_inst3) = Sil.hpara_instantiate para2 _e2 _f2 elist2 in

infer/src/backend/specs.ml

@@ -288,7 +288,7 @@ type call_stats = CallStats.t
 (** Execution statistics *)
 type stats =
   { stats_time: float; (** Analysis time for the procedure *)
-    stats_timeout: bool; (** Flag to indicate whether a timeout occurred *)
+    stats_failure: failure_kind option; (** what type of failure stopped the analysis (if any) *)
     stats_calls: Cg.in_out_calls; (** num of procs calling, and called *)
     symops: int; (** Number of SymOp's throughout the whole analysis of the function *)
     mutable nodes_visited_fp : IntSet.t; (** Nodes visited during the footprint phase *)
@@ -342,12 +342,14 @@ let pp_time whole_seconds fmt t =
   if whole_seconds then F.fprintf fmt "%3.0f s" t
   else F.fprintf fmt "%f s" t
 
-let pp_timeout fmt = function
+let pp_failure_kind_opt fmt failure_kind_opt = match failure_kind_opt with
-  | true -> F.fprintf fmt "Y"
+  | Some failure_kind -> pp_failure_kind fmt failure_kind
-  | false -> F.fprintf fmt "N"
+  | None -> F.fprintf fmt "NONE"
 
 let pp_stats err_log whole_seconds fmt stats =
-  F.fprintf fmt "TIME:%a TIMEOUT:%a SYMOPS:%d CALLS:%d,%d@\n" (pp_time whole_seconds) stats.stats_time pp_timeout stats.stats_timeout stats.symops stats.stats_calls.Cg.in_calls stats.stats_calls.Cg.out_calls;
+  F.fprintf fmt "TIME:%a FAILURE:%a SYMOPS:%d CALLS:%d,%d@\n" (pp_time whole_seconds)
+    stats.stats_time pp_failure_kind_opt stats.stats_failure stats.symops
+    stats.stats_calls.Cg.in_calls stats.stats_calls.Cg.out_calls;
   F.fprintf fmt "ERRORS: @[<h>%a@]@." Errlog.pp_errors err_log;
   F.fprintf fmt "WARNINGS: @[<h>%a@]" Errlog.pp_warnings err_log
 
@@ -463,7 +465,7 @@ let pp_spec_table pe whole_seconds fmt () =
 
 let empty_stats calls cyclomatic in_out_calls_opt =
   { stats_time = 0.0;
-    stats_timeout = false;
+    stats_failure = None;
     stats_calls =
       (match in_out_calls_opt with
        | Some in_out_calls -> in_out_calls
@@ -737,7 +739,7 @@ let get_iterations proc_name =
       try
         let time_str = Hashtbl.find proc_flags proc_flag_iterations in
         Pervasives.int_of_string time_str
-      with exn when exn_not_timeout exn -> !iterations_cmdline
+      with exn when exn_not_failure exn -> !iterations_cmdline
 
 (** Return the specs and parameters for the proc in the spec table *)
 let get_specs_formals proc_name =

infer/src/backend/specs.mli

@@ -102,7 +102,7 @@ end
 (** Execution statistics *)
 type stats =
   { stats_time: float; (** Analysis time for the procedure *)
-    stats_timeout: bool; (** Flag to indicate whether a timeout occurred *)
+    stats_failure: failure_kind option; (** what type of failure stopped the analysis (if any) *)
     stats_calls: Cg.in_out_calls; (** num of procs calling, and called *)
     symops: int; (** Number of SymOp's throughout the whole analysis of the function *)
     mutable nodes_visited_fp : IntSet.t; (** Nodes visited during the footprint phase *)

infer/src/backend/state.ml

@@ -234,7 +234,7 @@ let extract_pre p tenv pdesc abstract_fun =
     Sil.sub_of_list (IList.map (fun id -> incr count; (id, Sil.Var (Ident.create_normal Ident.name_spec !count))) idlist) in
   let _, p' = Cfg.remove_locals_formals pdesc p in
   let pre, _ = Prop.extract_spec p' in
-  let pre' = try abstract_fun tenv pre with exn when exn_not_timeout exn -> pre in
+  let pre' = try abstract_fun tenv pre with exn when exn_not_failure exn -> pre in
   Prop.normalize (Prop.prop_sub sub pre')
 
 (** return the normalized precondition extracted form the last prop seen, if any

infer/src/backend/symExec.ml

@@ -654,7 +654,7 @@ let redirect_shared_ptr tenv cfg pname actual_params =
           let name = Mangled.to_string cl_name in
           name = "shared_ptr" || name = "__shared_ptr"
       | t -> false
-    with exn when exn_not_timeout exn -> false in
+    with exn when exn_not_failure exn -> false in
   (* We pattern match over some specific library function, *)
   (* so we make precise matching to distinghuis between *)
   (* references and pointers in C++ *)
@@ -1141,7 +1141,7 @@ and sym_exec_generated mask_errors cfg tenv pdesc instrs ppl =
   let exe_instr instr (p, path) =
     L.d_str "Executing Generated Instruction "; Sil.d_instr instr; L.d_ln ();
     try sym_exec cfg tenv pdesc instr p path
-    with exn when exn_not_timeout exn && mask_errors ->
+    with exn when exn_not_failure exn && mask_errors ->
       let err_name, _, ml_source, _ , _, _, _ = Exceptions.recognize_exception exn in
       let loc = (match ml_source with
           | Some (src, l, c) -> "at "^(src^" "^(string_of_int l))
@@ -1316,7 +1316,7 @@ and sym_exe_check_variadic_sentinel ?(fails_on_nil = false) cfg pdesc tenv prop
     let letderef = Sil.Letderef (tmp_id_deref, lexp, typ, loc) in
     try
       sym_exec_generated false cfg tenv pdesc [letderef] result
-    with e when exn_not_timeout e ->
+    with e when exn_not_failure e ->
       if not fails_on_nil then
         let deref_str = Localise.deref_str_nil_argument_in_variadic_method callee_pname nargs i in
         let err_desc =

infer/src/backend/tabulation.ml

@@ -403,7 +403,7 @@ let rec fsel_star_fld fsel1 fsel2 = match fsel1, fsel2 with
 
 and array_content_star se1 se2 =
   try sexp_star_fld se1 se2 with
-  | exn when exn_not_timeout exn -> se1 (* let postcondition override *)
+  | exn when exn_not_failure exn -> se1 (* let postcondition override *)
 
 and esel_star_fld esel1 esel2 = match esel1, esel2 with
   | [], esel2 -> (* don't know whether element is read or written in fun call with array *)
@@ -476,7 +476,7 @@ let sigma_star_fld (sigma1 : Sil.hpred list) (sigma2 : Sil.hpred list) : Sil.hpr
         end
   in
   try star sigma1 sigma2
-  with exn when exn_not_timeout exn ->
+  with exn when exn_not_failure exn ->
     L.d_str "cannot star ";
     Prop.d_sigma sigma1; L.d_str " and "; Prop.d_sigma sigma2;
     L.d_ln ();
@@ -510,7 +510,7 @@ let sigma_star_typ (sigma1 : Sil.hpred list) (typings2 : (Sil.exp * Sil.exp) lis
               | _ -> star sg1 typings2'
             end in
       try star sigma1 typings2
-      with exn when exn_not_timeout exn ->
+      with exn when exn_not_failure exn ->
         L.d_str "cannot star ";
         Prop.d_sigma sigma1; L.d_str " and "; Prover.d_typings typings2;
         L.d_ln ();

infer/src/backend/utils.ml

@@ -257,20 +257,27 @@ let pp_ml_location_opt fmt mloco =
     | None -> ()
     | Some mloc -> F.fprintf fmt "(%a)" pp_ml_location mloc
 
-(** {2 SymOp and Timeouts: units of symbolic execution} *)
+(** {2 SymOp and Failures: units of symbolic execution} *)
 
-type timeout_kind =
+type failure_kind =
-  | TOtime (* max time exceeded *)
+  | FKtimeout (* max time exceeded *)
-  | TOsymops of int (* max symop's exceeded *)
+  | FKsymops_timeout of int (* max symop's exceeded *)
-  | TOrecursion of int (* max recursion level exceeded *)
+  | FKrecursion_timeout of int (* max recursion level exceeded *)
+  | FKcrash of string (* uncaught exception or failed assertion *)
 
-(** Timeout exception *)
+(** failure that prevented analysis from finishing *)
-exception Timeout_exe of timeout_kind
+exception Analysis_failure_exe of failure_kind
 
-let exn_not_timeout = function
+let exn_not_failure = function
-  | Timeout_exe _ -> false
+  | Analysis_failure_exe _ -> false
   | _ -> true
 
+let pp_failure_kind fmt = function
+  | FKtimeout -> F.fprintf 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
+
 let symops_timeout, seconds_timeout =
   (* default timeout and long timeout are the same for now, but this will change shortly *)
   let default_symops_timeout = 333 in
@@ -358,7 +365,7 @@ module SymOp = struct
   let pay () =
     incr symop_count; incr symop_total;
     if !symop_count > !timeout_symops && !alarm_active
-    then raise (Timeout_exe (TOsymops !symop_count));
+    then raise (Analysis_failure_exe (FKsymops_timeout !symop_count));
     check_wallclock_alarm ()
 
   (** Reset the counters *)

infer/src/backend/utils.mli

@@ -154,7 +154,7 @@ val pp_current_time : Format.formatter -> unit -> unit
 (** Print the time in seconds elapsed since the beginning of the execution of the current command. *)
 val pp_elapsed_time : Format.formatter -> unit -> unit
 
-(** {2 SymOp and Timeouts: units of symbolic execution} *)
+(** {2 SymOp and Failures: units of symbolic execution} *)
 
 (** initial time of the analysis, i.e. when this module is loaded, gotten from Unix.time *)
 val initial_analysis_time : float
@@ -174,16 +174,19 @@ val get_timeout_seconds : unit -> int
 (** Set the timeout values in seconds and symops, computed as a multiple of the integer parameter *)
 val set_iterations : int -> unit
 
-type timeout_kind =
+type failure_kind =
-  | TOtime (* max time exceeded *)
+  | FKtimeout (* max time exceeded *)
-  | TOsymops of int (* max symop's exceeded *)
+  | FKsymops_timeout of int (* max symop's exceeded *)
-  | TOrecursion of int (* max recursion level exceeded *)
+  | FKrecursion_timeout of int (* max recursion level exceeded *)
+  | FKcrash of string (* uncaught exception or failed assertion *)
 
 (** Timeout exception *)
-exception Timeout_exe of timeout_kind
+exception Analysis_failure_exe of failure_kind
 
 (** check that the exception is not a timeout exception *)
-val exn_not_timeout : exn -> bool
+val exn_not_failure : exn -> bool
+
+val pp_failure_kind : Format.formatter -> failure_kind -> unit
 
 (** Count the number of symbolic operations *)
 module SymOp : sig