From c4f153947b7ad9783ca74b5616a747a1d86ab457 Mon Sep 17 00:00:00 2001
From: Jia Chen <grievejia@fb.com>
Date: Mon, 24 Jul 2017 15:24:46 -0700
Subject: [PATCH] Removed unused option `allow_missing_index_in_proc_call`

Reviewed By: jeremydubreil

Differential Revision: D5483686

fbshipit-source-id: 04cd10b
---
 infer/src/backend/prover.ml                   |  4 +-
 infer/src/base/Config.ml                      |  5 ---
 infer/src/base/Config.mli                     |  3 +-
 .../codetoanalyze/c/biabduction/abduce.c      | 42 +++++++++++++++++++
 4 files changed, 45 insertions(+), 9 deletions(-)

diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml
index 0848add75..d283cca83 100644
--- a/infer/src/backend/prover.ml
+++ b/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)
diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml
index b1e3cb106..ca1c6fb23 100644
--- a/infer/src/base/Config.ml
+++ b/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_"
diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli
index 2ee519922..5d1ee14de 100644
--- a/infer/src/base/Config.mli
+++ b/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
diff --git a/infer/tests/codetoanalyze/c/biabduction/abduce.c b/infer/tests/codetoanalyze/c/biabduction/abduce.c
index b8cbe98e4..3023d8d5d 100644
--- a/infer/tests/codetoanalyze/c/biabduction/abduce.c
+++ b/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);
+}