[biabduction] Delete SKIP_POINTER_DEREFERENCE issue type

Summary: This is unused so let's delete it.

Reviewed By: ezgicicek

Differential Revision: D22159060

fbshipit-source-id: f8b534bcd

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

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

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

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

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

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

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

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 *)