pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[biabduction] Delete condition always true/false in the biabduction checker

Browse Source 
Summary: This is not used, so let's delete it.

Reviewed By: jvillard

Differential Revision: D22018894

fbshipit-source-id: 33edd119c
master
Dulma Churchill 5 years ago committed by Facebook GitHub Bot
parent 566c650087
commit 24ec6e9f90
10 changed files with 1 additions and 63 deletions
Show Stats Download Patch File Download Diff File

2
infer/man/man1/infer-full.txt
Unescape View File

@ -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),

2
infer/man/man1/infer-report.txt
Unescape View File

@ -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),

2
infer/man/man1/infer.txt
Unescape View File

@ -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),

2
infer/src/base/Config.ml
Unescape View File

@ -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

2
infer/src/base/Config.mli
Unescape View File

@ -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

10
infer/src/base/IssueType.ml
Unescape View File

@ -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"]

4
infer/src/base/IssueType.mli
Unescape View File

@ -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

7
infer/src/biabduction/Exceptions.ml
Unescape View File

@ -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

2
infer/src/biabduction/Exceptions.mli
Unescape View File

@ -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

31
infer/src/biabduction/SymExec.ml
Unescape View File

@ -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) -> (

Write Preview
Loading…
Cancel
Save