diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 04593e8e0..eb3cef24c 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -484,7 +484,6 @@ OPTIONS SHELL_INJECTION (enabled by default), SHELL_INJECTION_RISK (enabled by default), SKIP_FUNCTION (disabled by default), - SKIP_POINTER_DEREFERENCE (disabled by default), SQL_INJECTION (enabled by default), SQL_INJECTION_RISK (enabled by default), STACK_VARIABLE_ADDRESS_ESCAPE (enabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 69081736c..060fecf5b 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -209,7 +209,6 @@ OPTIONS SHELL_INJECTION (enabled by default), SHELL_INJECTION_RISK (enabled by default), SKIP_FUNCTION (disabled by default), - SKIP_POINTER_DEREFERENCE (disabled by default), SQL_INJECTION (enabled by default), SQL_INJECTION_RISK (enabled by default), STACK_VARIABLE_ADDRESS_ESCAPE (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 8842f2aa4..9e134fc58 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -484,7 +484,6 @@ OPTIONS SHELL_INJECTION (enabled by default), SHELL_INJECTION_RISK (enabled by default), SKIP_FUNCTION (disabled by default), - SKIP_POINTER_DEREFERENCE (disabled by default), SQL_INJECTION (enabled by default), SQL_INJECTION_RISK (enabled by default), STACK_VARIABLE_ADDRESS_ESCAPE (enabled by default), diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index f850c774f..6b22c8d81 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -822,10 +822,6 @@ let retain_cycle = let skip_function = register_hidden ~enabled:false ~id:"SKIP_FUNCTION" Info Biabduction -let skip_pointer_dereference = - register ~enabled:false ~id:"SKIP_POINTER_DEREFERENCE" Info Biabduction (* TODO *) - ~user_documentation:"" - let shell_injection = register ~id:"SHELL_INJECTION" Error Quandary diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index e6bff623a..6cf049b67 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -294,8 +294,6 @@ val retain_cycle : t val skip_function : t -val skip_pointer_dereference : t - val shell_injection : t val shell_injection_risk : t diff --git a/infer/src/biabduction/Exceptions.ml b/infer/src/biabduction/Exceptions.ml index 16c099e6c..758ec86e2 100644 --- a/infer/src/biabduction/Exceptions.ml +++ b/infer/src/biabduction/Exceptions.ml @@ -71,8 +71,6 @@ exception Registered_observer_being_deallocated of Localise.error_desc * L.ocaml exception Skip_function of Localise.error_desc -exception Skip_pointer_dereference of Localise.error_desc * L.ocaml_pos - exception Symexec_memory_error of L.ocaml_pos exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * L.ocaml_pos @@ -167,8 +165,6 @@ let recognize_exception exn : IssueToReport.t = {issue_type= IssueType.failure_exe; description= Localise.no_desc; ocaml_pos= None} | Skip_function desc -> {issue_type= IssueType.skip_function; description= desc; ocaml_pos= None} - | Skip_pointer_dereference (desc, ocaml_pos) -> - {issue_type= IssueType.skip_pointer_dereference; description= desc; ocaml_pos= Some ocaml_pos} | Symexec_memory_error ocaml_pos -> { issue_type= IssueType.symexec_memory_error ; description= Localise.no_desc diff --git a/infer/src/biabduction/Exceptions.mli b/infer/src/biabduction/Exceptions.mli index c506cd60d..13aadae08 100644 --- a/infer/src/biabduction/Exceptions.mli +++ b/infer/src/biabduction/Exceptions.mli @@ -70,8 +70,6 @@ exception Registered_observer_being_deallocated of Localise.error_desc * Logging exception Skip_function of Localise.error_desc -exception Skip_pointer_dereference of Localise.error_desc * Logging.ocaml_pos - exception Symexec_memory_error of Logging.ocaml_pos exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * Logging.ocaml_pos diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index 99db12f26..5fea408e5 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -1271,10 +1271,11 @@ let exe_call_postprocess tenv ret_id callee_pname callee_attrs loc results = else if Localise.is_empty_vector_access_desc desc then raise (Exceptions.Empty_vector_access (desc, __POS__)) else raise (Exceptions.Null_dereference (desc, __POS__)) - | Dereference_error (Deref_undef (_, _, pos), desc, path_opt) -> - extend_path path_opt (Some pos) ; - raise (Exceptions.Skip_pointer_dereference (desc, __POS__)) - | Prover_checks _ | Cannot_combine | Missing_sigma_not_empty | Missing_fld_not_empty -> + | Dereference_error (Deref_undef _, _, _) + | Prover_checks _ + | Cannot_combine + | Missing_sigma_not_empty + | Missing_fld_not_empty -> assert false ) | [] -> (* no dereference error detected *)