diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index 243bbcd70..ed827f97d 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -147,6 +147,14 @@ let unsafe_unret = "<\"Unsafe_unretained\">" let weak = "<\"Weak\">" +(** letters used in the analysis output *) +let log_analysis_file = "F" +let log_analysis_procedure = "." +let log_analysis_wallclock_timeout = "T" +let log_analysis_symops_timeout = "S" +let log_analysis_recursion_timeout = "R" +let log_analysis_crash = "C" + (** Compile time configuration values *) diff --git a/infer/src/backend/config.mli b/infer/src/backend/config.mli index d2e6be075..5e0154d92 100644 --- a/infer/src/backend/config.mli +++ b/infer/src/backend/config.mli @@ -50,6 +50,12 @@ val incremental_procs : bool val inferconfig_file : string val initial_analysis_time : float val ivar_attributes : string +val log_analysis_file : string +val log_analysis_procedure : string +val log_analysis_wallclock_timeout : string +val log_analysis_symops_timeout : string +val log_analysis_recursion_timeout : string +val log_analysis_crash : string val max_recursion : int val meet_level : int val models_dir : string diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index 7e580fdc1..eb2b0b6dd 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -123,7 +123,21 @@ let output_json_makefile_stats clusters = let print_prolog () = match Config.cluster_cmdline with | None -> - L.stdout "Starting analysis (Infer version %s)@." Version.versionString; + L.stdout "Starting analysis (Infer version %s)@\n" Version.versionString; + L.stdout "@\n"; + L.stdout "legend:@\n"; + L.stdout " \"%s\" analyzing a file@\n" Config.log_analysis_file; + L.stdout " \"%s\" analyzing a procedure@\n" Config.log_analysis_procedure; + if Config.developer_mode then ( + L.stdout " \"%s\" analyzer crashed@\n" Config.log_analysis_crash; + L.stdout " \"%s\" timeout: procedure analysis took too much time@\n" + Config.log_analysis_wallclock_timeout; + L.stdout " \"%s\" timeout: procedure analysis took too many symbolic execution steps@\n" + Config.log_analysis_symops_timeout; + L.stdout " \"%s\" timeout: procedure analysis took too many recursive iterations@\n" + Config.log_analysis_recursion_timeout; + ); + L.stdout "@\n@?"; | Some clname -> L.stdout "Cluster %s@." clname let process_cluster_cmdline fname = diff --git a/infer/src/backend/logging.ml b/infer/src/backend/logging.ml index 44125cd35..351269865 100644 --- a/infer/src/backend/logging.ml +++ b/infer/src/backend/logging.ml @@ -201,21 +201,21 @@ let log_progress_simple text = F.fprintf Format.err_formatter "%s@?" text let log_progress_file () = - log_progress_simple "F" + log_progress_simple Config.log_analysis_file let log_progress_procedure () = - log_progress_simple "." + log_progress_simple Config.log_analysis_procedure let log_progress_timeout_event failure_kind = if Config.developer_mode then begin match failure_kind with | SymOp.FKtimeout -> - log_progress_simple "T" + log_progress_simple Config.log_analysis_wallclock_timeout | SymOp.FKsymops_timeout _ -> - log_progress_simple "S" + log_progress_simple Config.log_analysis_symops_timeout | SymOp.FKrecursion_timeout _ -> - log_progress_simple "R" - | SymOp.FKcrash _ -> - log_progress_simple "C" + log_progress_simple Config.log_analysis_recursion_timeout + | SymOp.FKcrash msg -> + log_progress_simple (Printf.sprintf "%s(%s)" Config.log_analysis_crash msg) end