From c61d2ba32f6c76e77355ef275259e29545db698f Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 27 May 2020 08:24:01 -0700 Subject: [PATCH] kill Config.analysis_stops Summary: The option was misleading as it only concerns the biabduction analysis. Moreover, this is a developer option, and one can already see it by removing filtering altogether. I think this option was added as the result of a user request, let's see if anyone notices. Reviewed By: ezgicicek Differential Revision: D21686526 fbshipit-source-id: ff383a0ca --- infer/man/man1/infer-full.txt | 8 ++------ infer/man/man1/infer-report.txt | 4 ++-- infer/man/man1/infer.txt | 4 ++-- infer/src/IR/Exceptions.ml | 7 +++---- infer/src/base/Config.ml | 7 ------- infer/src/base/Config.mli | 2 -- infer/src/base/IssueType.ml | 6 ++++-- infer/src/base/IssueType.mli | 4 ++-- 8 files changed, 15 insertions(+), 27 deletions(-) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 052a97615..970cb1011 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -351,13 +351,13 @@ OPTIONS disabling issue types does not make the corresponding checker not run. Available issue types are as follows: - ANALYSIS_STOPS (disabled by default), - ARRAY_OUT_OF_BOUNDS_L1 (disabled by default), + ARRAY_OUT_OF_BOUNDS_L1 (disabled by default), ARRAY_OUT_OF_BOUNDS_L2 (disabled by default), ARRAY_OUT_OF_BOUNDS_L3 (disabled by default), Abduction_case_not_implemented (enabled by default), Array_of_pointsto (enabled by default), Assert_failure (enabled by default), + BIABDUCTION_ANALYSIS_STOPS (disabled by default), BIABD_CONDITION_ALWAYS_FALSE (disabled by default), BIABD_CONDITION_ALWAYS_TRUE (disabled by default), BIABD_REGISTERED_OBSERVER_BEING_DEALLOCATED (enabled by @@ -1154,10 +1154,6 @@ INTERNAL OPTIONS Activates: Forget leaked memory during abstraction (Conversely: --no-allow-leak) - --analysis-stops - Activates: Issue a warning when the analysis stops (Conversely: - --no-analysis-stops) - --append-buck-flavors-reset Set --append-buck-flavors to the empty list. diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 64e6e713f..9a8a0060b 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -77,13 +77,13 @@ OPTIONS disabling issue types does not make the corresponding checker not run. Available issue types are as follows: - ANALYSIS_STOPS (disabled by default), - ARRAY_OUT_OF_BOUNDS_L1 (disabled by default), + ARRAY_OUT_OF_BOUNDS_L1 (disabled by default), ARRAY_OUT_OF_BOUNDS_L2 (disabled by default), ARRAY_OUT_OF_BOUNDS_L3 (disabled by default), Abduction_case_not_implemented (enabled by default), Array_of_pointsto (enabled by default), Assert_failure (enabled by default), + BIABDUCTION_ANALYSIS_STOPS (disabled by default), BIABD_CONDITION_ALWAYS_FALSE (disabled by default), BIABD_CONDITION_ALWAYS_TRUE (disabled by default), BIABD_REGISTERED_OBSERVER_BEING_DEALLOCATED (enabled by diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index e1c397296..e8740166d 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -351,13 +351,13 @@ OPTIONS disabling issue types does not make the corresponding checker not run. Available issue types are as follows: - ANALYSIS_STOPS (disabled by default), - ARRAY_OUT_OF_BOUNDS_L1 (disabled by default), + ARRAY_OUT_OF_BOUNDS_L1 (disabled by default), ARRAY_OUT_OF_BOUNDS_L2 (disabled by default), ARRAY_OUT_OF_BOUNDS_L3 (disabled by default), Abduction_case_not_implemented (enabled by default), Array_of_pointsto (enabled by default), Assert_failure (enabled by default), + BIABDUCTION_ANALYSIS_STOPS (disabled by default), BIABD_CONDITION_ALWAYS_FALSE (disabled by default), BIABD_CONDITION_ALWAYS_TRUE (disabled by default), BIABD_REGISTERED_OBSERVER_BEING_DEALLOCATED (enabled by diff --git a/infer/src/IR/Exceptions.ml b/infer/src/IR/Exceptions.ml index a5a9ee0c3..8c6043ab2 100644 --- a/infer/src/IR/Exceptions.ml +++ b/infer/src/IR/Exceptions.ml @@ -131,11 +131,10 @@ let recognize_exception exn = ; visibility= Exn_developer ; severity= None } | Analysis_stops (desc, ocaml_pos_opt) -> - let visibility = if Config.analysis_stops then Exn_user else Exn_developer in - { issue_type= IssueType.analysis_stops + { issue_type= IssueType.biabduction_analysis_stops ; description= desc ; ocaml_pos= ocaml_pos_opt - ; visibility + ; visibility= Exn_developer ; severity= None } | Array_of_pointsto ocaml_pos -> { issue_type= IssueType.array_of_pointsto @@ -208,7 +207,7 @@ let recognize_exception exn = ; visibility= Exn_user ; severity= None } | Dummy_exception desc -> - { issue_type= IssueType.analysis_stops + { issue_type= IssueType.biabduction_analysis_stops ; description= desc ; ocaml_pos= None ; visibility= Exn_developer diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index abd228898..cea5be583 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -519,11 +519,6 @@ and allow_leak = CLOpt.mk_bool ~deprecated:["leak"] ~long:"allow-leak" "Forget leaked memory during abstraction" -and analysis_stops = - CLOpt.mk_bool ~deprecated:["analysis_stops"] ~long:"analysis-stops" - "Issue a warning when the analysis stops" - - and analyzer = CLOpt.mk_symbol ~deprecated:["analyzer"; "-analyzer"; "a"] ~long:"" ~default:Checkers ~eq:equal_analyzer ~symbols:string_to_analyzer @@ -2564,8 +2559,6 @@ and abs_val = !abs_val and allow_leak = !allow_leak -and analysis_stops = !analysis_stops - and annotation_reachability_cxx = !annotation_reachability_cxx and annotation_reachability_cxx_sources = !annotation_reachability_cxx_sources diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index eb5f4fd32..c3b98c39b 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -160,8 +160,6 @@ val abs_val : int val allow_leak : bool -val analysis_stops : bool - val annotation_reachability_cxx : Yojson.Basic.t val annotation_reachability_cxx_sources : Yojson.Basic.t diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index dd7be6d9e..1f0830bc0 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -142,8 +142,6 @@ let abduction_case_not_implemented = register_from_string ~id:"Abduction_case_not_implemented" Biabduction -let analysis_stops = register_from_string ~enabled:false ~id:"ANALYSIS_STOPS" Biabduction - let array_of_pointsto = register_from_string ~id:"Array_of_pointsto" Biabduction let array_out_of_bounds_l1 = @@ -162,6 +160,10 @@ let assert_failure = register_from_string ~id:"Assert_failure" Biabduction let bad_footprint = register_from_string ~id:"Bad_footprint" Biabduction +let biabduction_analysis_stops = + register_from_string ~enabled:false ~id:"BIABDUCTION_ANALYSIS_STOPS" Biabduction + + let biabd_condition_always_false = register_from_string ~enabled:false ~hum:"Condition Always False" ~id:"BIABD_CONDITION_ALWAYS_FALSE" Biabduction diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 2e13ac2d8..9b429cf41 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -50,8 +50,6 @@ val set_enabled : t -> bool -> unit val abduction_case_not_implemented : t -val analysis_stops : t - val array_of_pointsto : t val array_out_of_bounds_l1 : t @@ -64,6 +62,8 @@ val assert_failure : t val bad_footprint : t +val biabduction_analysis_stops : t + val biabd_condition_always_false : t val biabd_condition_always_true : t