[inferbo] Revise std::array::at model

Reviewed By: mbouaziz

Differential Revision: D13814848

fbshipit-source-id: c03153927

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -412,7 +412,9 @@ module StdArray = struct
     (* TODO? use size *)
     let exec {integer_type_widths} ~ret:(id, _) mem =
       L.d_printfln_escaped "Using model std::array<_, %Ld>::at" _size ;
-      BoUtils.Exec.load_val id (Sem.eval_lindex integer_type_widths array_exp index_exp mem) mem
+      Dom.Mem.add_stack (Loc.of_id id)
+        (Sem.eval_lindex integer_type_widths array_exp index_exp mem)
+        mem
     and check {location; integer_type_widths} mem cond_set =
       BoUtils.Check.lindex integer_type_widths ~array_exp ~index_exp ~last_included:false mem
         location cond_set

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -44,8 +44,6 @@ module Exec = struct
     else mem
 
 
-  let load_val id v mem = load_locs id (Dom.Val.get_all_locs v) mem
-
   let rec decl_local_loc ({tenv} as model_env) loc typ ~inst_num ~represents_multiple_values
       ~dimension mem =
     match typ.Typ.desc with

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -26,8 +26,6 @@ end
 module Exec : sig
   val load_locs : Ident.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t
 
-  val load_val : Ident.t -> Dom.Val.t -> Dom.Mem.t -> Dom.Mem.t
-
   val decl_local : ModelEnv.model_env -> Dom.Mem.t * int -> Loc.t * Typ.t -> Dom.Mem.t * int
 
   val init_c_array_fields :

infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp

@@ -84,6 +84,7 @@ codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INFERBO_ALLOC_IS
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<RHS trace>,Assignment,Binary operation: (4 × 18446744073709551615):unsigned64]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
+codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_contents_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, call_length4_1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Array declaration,Array access: Offset: 11 Size: 10 by call to `length4` ]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, call_length4_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Length trace>,Array declaration,Array access: Offset: 11 Size: 10 by call to `length4` ]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, compare_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]

infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp

@@ -46,7 +46,7 @@ void std_array_contents_Good() {
   a[a[0]] = 0;
 }
 
-void std_array_contents_Bad_FN() {
+void std_array_contents_Bad() {
   std::array<int, 10> a;
   a[0] = 10;
   a[a[0]] = 0;