diff --git a/infer/src/backend/logging.ml b/infer/src/backend/logging.ml index 1b3244c4a..064c0ca13 100644 --- a/infer/src/backend/logging.ml +++ b/infer/src/backend/logging.ml @@ -181,3 +181,17 @@ let log_progress_file () = let log_progress_procedure () = log_progress_simple "." + +let log_progress_timeout_event failure_kind = + if !Config.developer_mode then + begin + match failure_kind with + | FKtimeout -> + log_progress_simple "T" + | FKsymops_timeout _ -> + log_progress_simple "S" + | FKrecursion_timeout _ -> + log_progress_simple "R" + | FKcrash _ -> + log_progress_simple "C" + end diff --git a/infer/src/backend/logging.mli b/infer/src/backend/logging.mli index 948fa336e..edd26c474 100644 --- a/infer/src/backend/logging.mli +++ b/infer/src/backend/logging.mli @@ -135,3 +135,6 @@ val log_progress_file : unit -> unit (** Progress bar: start of the analysis of a procedure. *) val log_progress_procedure : unit -> unit + +(** Progress bar: log a timeout event if in developer mode. *) +val log_progress_timeout_event : failure_kind -> unit diff --git a/infer/src/backend/timeout.ml b/infer/src/backend/timeout.ml index 1dbb31a9d..f71c6f1f2 100644 --- a/infer/src/backend/timeout.ml +++ b/infer/src/backend/timeout.ml @@ -119,6 +119,7 @@ let exe_timeout f x = with | Analysis_failure_exe kind -> resume_previous_timeout (); + L.log_progress_timeout_event kind; Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." pp_failure_kind kind; Some kind | exe ->