diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index ba02956aa..72666c491 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -371,8 +371,6 @@ OPTIONS BAD_POINTER_COMPARISON (enabled by default), BIABDUCTION_ANALYSIS_STOPS (disabled by default), BIABDUCTION_MEMORY_LEAK (disabled by default), - BIABD_CONDITION_ALWAYS_FALSE (disabled by default), - BIABD_CONDITION_ALWAYS_TRUE (disabled by default), BUFFER_OVERRUN_L1 (enabled by default), BUFFER_OVERRUN_L2 (enabled by default), BUFFER_OVERRUN_L3 (enabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 9d18332db..2ced7a413 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -91,8 +91,6 @@ OPTIONS BAD_POINTER_COMPARISON (enabled by default), BIABDUCTION_ANALYSIS_STOPS (disabled by default), BIABDUCTION_MEMORY_LEAK (disabled by default), - BIABD_CONDITION_ALWAYS_FALSE (disabled by default), - BIABD_CONDITION_ALWAYS_TRUE (disabled by default), BUFFER_OVERRUN_L1 (enabled by default), BUFFER_OVERRUN_L2 (enabled by default), BUFFER_OVERRUN_L3 (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index e5bebd4d8..3bc2c395c 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -371,8 +371,6 @@ OPTIONS BAD_POINTER_COMPARISON (enabled by default), BIABDUCTION_ANALYSIS_STOPS (disabled by default), BIABDUCTION_MEMORY_LEAK (disabled by default), - BIABD_CONDITION_ALWAYS_FALSE (disabled by default), - BIABD_CONDITION_ALWAYS_TRUE (disabled by default), BUFFER_OVERRUN_L1 (enabled by default), BUFFER_OVERRUN_L2 (enabled by default), BUFFER_OVERRUN_L3 (enabled by default), diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 628e7635a..ca11cc52c 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -172,8 +172,6 @@ let nsnotification_center_checker_backend = false let property_attributes = "property_attributes" -let report_condition_always_true_in_clang = false - (** If true, sanity-check inferred preconditions against Nullable annotations and report inconsistencies *) let report_nullable_inconsistency = true diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 0179904c0..a10869fac 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -114,8 +114,6 @@ val relative_path_backtrack : int val report : bool -val report_condition_always_true_in_clang : bool - val report_custom_error : bool val report_force_relative_path : bool diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index dc48846b3..e88067e2c 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -259,16 +259,6 @@ let biabduction_analysis_stops = Biabduction -let biabd_condition_always_false = - register_from_string ~enabled:false ~hum:"Condition Always False" - ~id:"BIABD_CONDITION_ALWAYS_FALSE" Warning Biabduction - - -let biabd_condition_always_true = - register_from_string ~enabled:false ~hum:"Condition Always True" ~id:"BIABD_CONDITION_ALWAYS_TRUE" - Warning Biabduction - - let buffer_overrun_l1 = register_from_string ~id:"BUFFER_OVERRUN_L1" Error BufferOverrunChecker ~user_documentation:[%blob "../../documentation/issues/BUFFER_OVERRUN.md"] diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index c9a45bcf1..ec9f551ab 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -85,10 +85,6 @@ val bad_footprint : t val biabduction_analysis_stops : t -val biabd_condition_always_false : t - -val biabd_condition_always_true : t - val buffer_overrun_l1 : t val buffer_overrun_l2 : t diff --git a/infer/src/biabduction/Exceptions.ml b/infer/src/biabduction/Exceptions.ml index d8dda7903..27fe30148 100644 --- a/infer/src/biabduction/Exceptions.ml +++ b/infer/src/biabduction/Exceptions.ml @@ -30,8 +30,6 @@ exception Cannot_star of L.ocaml_pos exception Class_cast_exception of Localise.error_desc * L.ocaml_pos -exception Condition_always_true_false of Localise.error_desc * bool * L.ocaml_pos - exception Custom_error of string * IssueType.severity * Localise.error_desc exception @@ -114,11 +112,6 @@ let recognize_exception exn : IssueToReport.t = {issue_type= IssueType.cannot_star; description= Localise.no_desc; ocaml_pos= Some ocaml_pos} | Class_cast_exception (desc, ocaml_pos) -> {issue_type= IssueType.class_cast_exception; description= desc; ocaml_pos= Some ocaml_pos} - | Condition_always_true_false (desc, b, ocaml_pos) -> - let issue_type = - if b then IssueType.biabd_condition_always_true else IssueType.biabd_condition_always_false - in - {issue_type; description= desc; ocaml_pos= Some ocaml_pos} | Custom_error (error_msg, severity, desc) -> { issue_type= IssueType.register_from_string ~id:error_msg severity Biabduction ; description= desc diff --git a/infer/src/biabduction/Exceptions.mli b/infer/src/biabduction/Exceptions.mli index fca2aba4d..1176bc42c 100644 --- a/infer/src/biabduction/Exceptions.mli +++ b/infer/src/biabduction/Exceptions.mli @@ -28,8 +28,6 @@ exception Cannot_star of Logging.ocaml_pos exception Class_cast_exception of Localise.error_desc * Logging.ocaml_pos -exception Condition_always_true_false of Localise.error_desc * bool * Logging.ocaml_pos - exception Custom_error of string * IssueType.severity * Localise.error_desc exception diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 14c46f4a7..097f70aa9 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -1212,39 +1212,10 @@ let rec sym_exec execute_load analysis_data id rhs_exp typ loc prop_ |> ret_old_path | Sil.Store {e1= lhs_exp; root_typ= typ; e2= rhs_exp; loc} -> execute_store analysis_data lhs_exp typ rhs_exp loc prop_ |> ret_old_path - | Sil.Prune (cond, loc, true_branch, ik) -> + | Sil.Prune (cond, _, _, _) -> let prop__ = Attribute.nullify_exp_with_objc_null tenv prop_ cond in - let check_condition_always_true_false () = - if (not (Language.curr_language_is Clang)) || Config.report_condition_always_true_in_clang - then - let report_condition_always_true_false i = - let skip_loop = - match ik with - | Sil.Ik_while | Sil.Ik_for -> - not (IntLit.iszero i) (* skip while(1) and for (;1;) *) - | Sil.Ik_dowhile -> - true (* skip do..while *) - | Sil.Ik_land_lor -> - true (* skip subpart of a condition obtained from compilation of && and || *) - | _ -> - false - in - true_branch && not skip_loop - in - match Prop.exp_normalize_prop tenv Prop.prop_emp cond with - | Exp.Const (Const.Cint i) when report_condition_always_true_false i -> - let node = AnalysisState.get_node_exn () in - let desc = Errdesc.explain_condition_always_true_false tenv i cond node loc in - let exn = - Exceptions.Condition_always_true_false (desc, not (IntLit.iszero i), __POS__) - in - BiabductionReporting.log_issue_deprecated_using_state current_pdesc err_log exn - | _ -> - () - in if not (Procname.is_java current_pname) then check_already_dereferenced analysis_data cond prop__ ; - check_condition_always_true_false () ; let n_cond, prop = check_arith_norm_exp analysis_data cond prop__ in ret_old_path (Propset.to_proplist (prune tenv ~positive:true n_cond prop)) | Sil.Call (ret_id_typ, Exp.Const (Const.Cfun callee_pname), actual_params, loc, call_flags) -> (