From 9de3f9792cf43d536cb0ecf0e53995db342142ae Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 11 May 2016 14:25:26 -0700 Subject: [PATCH] print legend for the output Summary: F for files, . for procedures, and a few more for developer mode. Also add the crash message to the crash symbol, because if infer crashes we want as much information as possible. ``` $ infer -- javac Hello.java Starting analysis (Infer version v0.8.1-8e8c6fa) legend: "F" analyzing a file "." analyzing a procedure F.. Analyzed 1 file Found 1 issue Hello.java:13: error: NULL_DEREFERENCE object s last assigned on line 12 could be null and is dereferenced at line 13 11. int test() { 12. String s = null; 13. > return s.length(); 14. } 15. } 16. Summary of the reports NULL_DEREFERENCE: 1 $ infer -g -- javac Hello.java ... Starting analysis (Infer version v0.8.1-8e8c6fa) legend: "F" analyzing a file "." analyzing a procedure "C" analyzer crashed "T" timeout: procedure analysis took too much time "S" timeout: procedure analysis took too many symbolic execution steps "R" timeout: procedure analysis took too many recursive iterations ... ``` Reviewed By: sblackshear Differential Revision: D3288081 fbshipit-source-id: becea34 --- infer/src/backend/config.ml | 8 ++++++++ infer/src/backend/config.mli | 6 ++++++ infer/src/backend/inferanalyze.ml | 16 +++++++++++++++- infer/src/backend/logging.ml | 14 +++++++------- 4 files changed, 36 insertions(+), 8 deletions(-) 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