Removed unused option `allow_missing_index_in_proc_call`

Reviewed By: jeremydubreil

Differential Revision: D5483686

fbshipit-source-id: 04cd10b

infer/src/backend/prover.ml

@@ -1478,8 +1478,8 @@ let rec sexp_imply tenv source calc_index_frame calc_missing subs se1 se2 typ2
         if index_frame <> [] then Some (Sil.Earray (len1, index_frame, inst1)) else None
       in
       let index_missing_opt =
-        if index_missing <> [] && (Config.allow_missing_index_in_proc_call || !Config.footprint)
-        then Some (Sil.Earray (len1, index_missing, inst1))
+        if index_missing <> [] && !Config.footprint then
+          Some (Sil.Earray (len1, index_missing, inst1))
         else None
       in
       (subs'', index_frame_opt, index_missing_opt)

infer/src/base/Config.ml

@@ -83,11 +83,6 @@ type os_type = Unix | Win32 | Cygwin
 
 (** Constant configuration values *)
 
-(** If true, a precondition with e.g. index 3 in an array does not require the caller to
-    have index 3 too this mimics what happens with direct access to the array without a
-    procedure call, where the index is simply materialized if not there *)
-let allow_missing_index_in_proc_call = true
-
 let anonymous_block_num_sep = "______"
 
 let anonymous_block_prefix = "__objc_anonymous_block_"

infer/src/base/Config.mli

@@ -71,8 +71,6 @@ val env_inside_maven : Unix.env
 
 (** Constant configuration values *)
 
-val allow_missing_index_in_proc_call : bool
-
 val anonymous_block_num_sep : string
 
 val anonymous_block_prefix : string
@@ -216,6 +214,7 @@ val specs_dir_name : string
 val specs_files_suffix : string
 
 val start_filename : string
+
 val trace_absarray : bool
 
 val undo_join : bool

infer/tests/codetoanalyze/c/biabduction/abduce.c

@@ -13,3 +13,45 @@ int const_local_no_abduce(int* p) {
   return p ? *p : 0;
   // We shouldn't get a stack address escape warning here
 }
+
+void set_ptr(int* ptr, int val) { *ptr = val; }
+
+int set_ptr_local_array() {
+  int buf[2];
+  set_ptr(buf, 1);
+  return buf[0];
+}
+
+void set_ptr_local_array_return_true_ok() {
+  int* p = 0;
+  if (!set_ptr_local_array())
+    // not reachable if the analysis of set_ptr_local_array is correct
+    *p = 42;
+}
+
+int set_ptr_param_array(int buf[]) {
+  set_ptr(buf, 1);
+  return buf[0];
+}
+
+void set_ptr_param_array_return_true_ok() {
+  int buf[2];
+  int* p = 0;
+  if (!set_ptr_param_array(buf))
+    // not reachable if the analysis of set_ptr_local_array is correct
+    *p = 42;
+}
+
+void set_ptr_param_array_get_ptr_ok() {
+  int x = 0;
+  int* p = 0;
+  if (!set_ptr_param_array(&x))
+    // not reachable if the analysis of set_ptr_local_array is correct
+    *p = 42;
+}
+
+void FN_set_ptr_param_array_get_null_bad() {
+  // A null pointer dereference is expected here, but currently we get a
+  // PRECONDITION_NOT_MET
+  set_ptr_param_array(0);
+}