[inferbo] Weak update for array contents

Summary: It weakly updates array when there are more than two contents.

Reviewed By: mbouaziz

Differential Revision: D13318443

fbshipit-source-id: fa740d8b1

infer/src/bufferoverrun/absLoc.ml

@@ -19,6 +19,7 @@ module Allocsite = struct
         ; node_hash: int
         ; inst_num: int
         ; dimension: int
+        ; represents_multiple_values: bool
         ; path: Symb.SymbolPath.partial option }
   [@@deriving compare]
 
@@ -63,9 +64,16 @@ module Allocsite = struct
       -> inst_num:int
       -> dimension:int
       -> path:Symb.SymbolPath.partial option
+      -> represents_multiple_values:bool
       -> t =
-   fun proc_name ~node_hash ~inst_num ~dimension ~path ->
+   fun proc_name ~node_hash ~inst_num ~dimension ~path ~represents_multiple_values ->
-    Known {proc_name= Typ.Procname.to_string proc_name; node_hash; inst_num; dimension; path}
+    Known
+      { proc_name= Typ.Procname.to_string proc_name
+      ; node_hash
+      ; inst_num
+      ; dimension
+      ; path
+      ; represents_multiple_values }
 
 
   let make_symbol path = Symbol path
@@ -79,6 +87,16 @@ module Allocsite = struct
         Option.some_if (not (Symb.SymbolPath.represents_callsite_sound_partial path)) path
     | Unknown | Known _ ->
         None
+
+
+  let represents_multiple_values = function
+    | Unknown ->
+        false
+    | Symbol path ->
+        Symb.SymbolPath.represents_multiple_values path
+    | Known {path; represents_multiple_values} ->
+        represents_multiple_values
+        || Option.value_map path ~default:false ~f:Symb.SymbolPath.represents_multiple_values
 end
 
 module Loc = struct
@@ -179,6 +197,15 @@ module Loc = struct
     Option.value_map (get_path x) ~default:false ~f:(fun x ->
         Option.value_map (Symb.SymbolPath.get_pvar x) ~default:false ~f:(fun x ->
             List.exists formals ~f:(fun (formal, _) -> Pvar.equal x formal) ) )
+
+
+  let rec represents_multiple_values = function
+    | Var _ ->
+        false
+    | Allocsite allocsite ->
+        Allocsite.represents_multiple_values allocsite
+    | Field (l, _) ->
+        represents_multiple_values l
 end
 
 module PowLoc = struct
@@ -213,8 +240,7 @@ module PowLoc = struct
     fold (fun l acc -> join acc (subst_loc l eval_locpath)) x empty
 end
 
-(** unsound but ok for bug catching *)
+let always_strong_update = false
-let always_strong_update = true
 
 let can_strong_update : PowLoc.t -> bool =
  fun ploc ->

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -855,14 +855,16 @@ module MemReach = struct
 
   let find_stack : Loc.t -> t -> Val.t = fun l m -> Option.value (find_opt l m) ~default:Val.bot
 
-  let find_heap : default:Val.t -> Loc.t -> t -> Val.t =
+  let find_heap_default : default:Val.t -> Loc.t -> t -> Val.t =
    fun ~default l m ->
     IOption.value_default_f (find_opt l m) ~f:(fun () ->
         Option.value_map m.oenv ~default ~f:(fun oenv -> Val.on_demand ~default oenv l) )
 
 
+  let find_heap : Loc.t -> t -> Val.t = find_heap_default ~default:Val.Itv.top
+
   let find : Loc.t -> t -> Val.t =
-   fun l m -> if is_stack_loc l m then find_stack l m else find_heap ~default:Val.Itv.top l m
+   fun l m -> if is_stack_loc l m then find_stack l m else find_heap l m
 
 
   let find_set : PowLoc.t -> t -> Val.t =
@@ -933,19 +935,27 @@ module MemReach = struct
     PowLoc.fold strong_update1 locs m
 
 
-  let transform_mem : f:(Val.t -> Val.t) -> PowLoc.t -> t -> t =
+  let transformi_mem : f:(Loc.t -> Val.t -> Val.t) -> PowLoc.t -> t -> t =
    fun ~f locs m ->
     let transform_mem1 l m =
       let add, find =
         if is_stack_loc l m then (replace_stack, find_stack)
-        else (add_heap, find_heap ~default:Val.bot)
+        else (add_heap, find_heap_default ~default:Val.bot)
       in
-      add l (f (find l m)) m
+      add l (f l (find l m)) m
     in
     PowLoc.fold transform_mem1 locs m
 
 
-  let weak_update locs v m = transform_mem ~f:(fun v' -> Val.join v' v) locs m
+  let transform_mem : f:(Val.t -> Val.t) -> PowLoc.t -> t -> t =
+   fun ~f -> transformi_mem ~f:(fun _ v -> f v)
+
+
+  let weak_update locs v m =
+    transformi_mem
+      ~f:(fun l v' -> if Loc.represents_multiple_values l then Val.join v' v else v)
+      locs m
+
 
   let update_mem : PowLoc.t -> Val.t -> t -> t =
    fun ploc v s ->
@@ -1138,8 +1148,6 @@ module Mem = struct
 
   let strong_update : PowLoc.t -> Val.t -> t -> t = fun p v -> f_lift (MemReach.strong_update p v)
 
-  let weak_update : PowLoc.t -> Val.t -> t -> t = fun p v -> f_lift (MemReach.weak_update p v)
-
   let get_reachable_locs_from : (Pvar.t * Typ.t) list -> PowLoc.t -> t -> PowLoc.t =
    fun formals locs ->
     f_lift_default ~default:PowLoc.empty (MemReach.get_reachable_locs_from formals locs)

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -88,17 +88,6 @@ let check_alloc_size size_exp {location; integer_type_widths} mem cond_set =
       PO.ConditionSet.add_alloc_size location ~length traces cond_set
 
 
-let set_uninitialized location (typ : Typ.t) ploc mem =
-  match typ.desc with
-  | Tint _ | Tfloat _ ->
-      Dom.Mem.weak_update ploc Dom.Val.Itv.top mem
-  | _ ->
-      L.(debug BufferOverrun Verbose)
-        "/!\\ Do not know how to uninitialize type %a at %a@\n" (Typ.pp Pp.text) typ Location.pp
-        location ;
-      mem
-
-
 let malloc size_exp =
   let exec {pname; node_hash; location; tenv; integer_type_widths} ~ret:(id, _) mem =
     let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in
@@ -106,8 +95,11 @@ let malloc size_exp =
     let length = Sem.eval integer_type_widths length0 mem in
     let traces = Trace.(Set.add_elem location ArrayDeclaration) (Dom.Val.get_traces length) in
     let path = Option.bind (Dom.Mem.find_simple_alias id mem) ~f:Loc.get_path in
-    let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in
     let offset, size = (Itv.zero, Dom.Val.get_itv length) in
+    let allocsite =
+      let represents_multiple_values = not (Itv.is_one size) in
+      Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path ~represents_multiple_values
+    in
     let size_exp_opt =
       let size_exp = Option.value dyn_length ~default:length0 in
       Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) size_exp
@@ -116,7 +108,6 @@ let malloc size_exp =
     mem
     |> Dom.Mem.add_stack (Loc.of_id id) v
     |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt
-    |> set_uninitialized location typ (Dom.Val.get_array_locs v)
     |> BoUtils.Exec.init_array_fields tenv integer_type_widths pname path ~node_hash typ
          (Dom.Val.get_array_locs v) ?dyn_length
   and check = check_alloc_size size_exp in
@@ -251,17 +242,19 @@ let get_array_length array_exp =
 let set_array_length array length_exp =
   let exec {pname; node_hash; location; integer_type_widths} ~ret:_ mem =
     match array with
-    | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} ->
+    | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {stride}} ->
         let length = Sem.eval integer_type_widths length_exp mem in
         let stride = Option.map ~f:IntLit.to_int_exn stride in
         let path = Some (Symb.SymbolPath.of_pvar array_pvar) in
-        let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in
         let traces = Trace.(Set.add_elem location ArrayDeclaration) (Dom.Val.get_traces length) in
         let size = Dom.Val.get_itv length in
+        let allocsite =
+          let represents_multiple_values = not (Itv.is_one size) in
+          Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path
+            ~represents_multiple_values
+        in
         let v = Dom.Val.of_array_alloc allocsite ~stride ~offset:Itv.zero ~size ~traces in
-        mem
+        Dom.Mem.add_stack (Loc.of_pvar array_pvar) v mem
-        |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v
-        |> set_uninitialized location elt (Dom.Val.get_array_locs v)
     | _ ->
         L.(die InternalError) "Unexpected type of first argument for __set_array_length() "
   and check = check_alloc_size length_exp in
@@ -386,7 +379,10 @@ module Collection = struct
     let exec {pname; node_hash; location} ~ret:(id, _) mem =
       let loc = Loc.of_id id in
       let path = Option.bind (Dom.Mem.find_simple_alias id mem) ~f:Loc.get_path in
-      let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in
+      let allocsite =
+        Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path
+          ~represents_multiple_values:true
+      in
       let alloc_loc = Loc.of_allocsite allocsite in
       let init_size = Dom.Val.of_int 0 in
       let traces = Trace.(Set.singleton location ArrayDeclaration) in

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -67,7 +67,10 @@ module Exec = struct
     let offset = Itv.zero in
     let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in
     let path = Loc.get_path loc in
-    let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension ~path in
+    let allocsite =
+      let represents_multiple_values = represents_multiple_values || not (Itv.is_one size) in
+      Allocsite.make pname ~node_hash ~inst_num ~dimension ~path ~represents_multiple_values
+    in
     let mem =
       let arr =
         let traces = Trace.(Set.singleton location ArrayDeclaration) in
@@ -97,7 +100,9 @@ module Exec = struct
       -> Dom.Mem.t * int =
    fun pname ~node_hash location loc ~inst_num ~represents_multiple_values ~dimension mem ->
     let path = Loc.get_path loc in
-    let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension ~path in
+    let allocsite =
+      Allocsite.make pname ~node_hash ~inst_num ~dimension ~path ~represents_multiple_values:true
+    in
     let alloc_loc = Loc.of_allocsite allocsite in
     let traces = Trace.(Set.singleton location ArrayDeclaration) in
     let mem =
@@ -185,7 +190,9 @@ module Exec = struct
             in
             let stride = Option.map stride ~f:IntLit.to_int_exn in
             let allocsite =
+              let represents_multiple_values = not (Itv.is_one length) in
               Allocsite.make pname ~node_hash ~inst_num ~dimension ~path:field_path
+                ~represents_multiple_values
             in
             let offset, size = (Itv.zero, length) in
             let v =

infer/src/bufferoverrun/itv.ml

@@ -559,6 +559,8 @@ let get_iterator_itv : t -> t = lift1 ItvPure.get_iterator_itv
 
 let is_const : t -> Z.t option = bind1zo ItvPure.is_const
 
+let is_one = bind1bool ItvPure.is_one
+
 let is_mone = bind1bool ItvPure.is_mone
 
 let eq_const : Z.t -> t -> bool = fun z -> bind1bool (ItvPure.eq_const z)

infer/src/bufferoverrun/itv.mli

@@ -137,6 +137,8 @@ val of_int64 : Int64.t -> t
 
 val is_const : t -> Z.t option
 
+val is_one : t -> bool
+
 val is_mone : t -> bool
 
 val eq_const : Z.t -> t -> bool

infer/tests/codetoanalyze/c/bufferoverrun/array_content.c

@@ -52,3 +52,54 @@ void call_array_min_index_from_one_good() {
   int a[2];
   a[array_min_index_from_one_FP(a, 2) - 1] = 0;
 }
+
+void weak_update_Good_FP() {
+  int a[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 15};
+  a[a[3]] = 3;
+}
+
+void weak_update_Bad() {
+  int a[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
+  if (a[0] == 0) {
+    a[15] = 1;
+  }
+}
+
+void strong_update_malloc_Good() {
+  int a[10];
+  int* x = (int*)malloc(sizeof(int));
+  *x = 10;
+  *x = 0;
+  a[*x] = 0;
+}
+
+void strong_update_malloc_Bad() {
+  int a[10];
+  int* x = (int*)malloc(sizeof(int));
+  *x = 0;
+  *x = 10;
+  a[*x] = 0;
+}
+
+void weak_update_malloc_Good_FP() {
+  int a[10];
+  int* x = (int*)malloc(sizeof(int) * 2);
+  x[0] = 0;
+  x[1] = 10;
+  a[x[0]] = 0;
+}
+
+void weak_update_malloc_Bad() {
+  int a[10];
+  int* x = (int*)malloc(sizeof(int) * 2);
+  x[0] = 0;
+  x[1] = 10;
+  a[x[1]] = 0;
+}
+
+void weak_update_malloc2_Bad_FN() {
+  int a[10];
+  int* x = (int*)malloc(sizeof(int) * 2);
+  x[0] = 0;
+  a[x[1]] = 0;
+}

infer/tests/codetoanalyze/c/bufferoverrun/array_multidim.c

@@ -57,7 +57,7 @@ void multidim_arr5_Bad() {
   a[0][10] = 0;
 }
 
-void multidim_arr6_Good() {
+void multidim_arr6_Good_FP() {
   int a[3][2];
   int b[10];
   int* p = a;
@@ -65,7 +65,7 @@ void multidim_arr6_Good() {
   b[a[0][0]] = 1;
 }
 
-void multidim_arr6_Bad_FN() {
+void multidim_arr6_Bad() {
   int a[3][2];
   int b[5];
   int* p = a;

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

@@ -46,13 +46,20 @@ codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, C
 codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/array_content.c, strong_update_malloc_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/c/bufferoverrun/array_content.c, weak_update_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 15 Size: 10]
+codetoanalyze/c/bufferoverrun/array_content.c, weak_update_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 15] Size: 10]
+codetoanalyze/c/bufferoverrun/array_content.c, weak_update_malloc_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 10]
+codetoanalyze/c/bufferoverrun/array_content.c, weak_update_malloc_Good_FP, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 10]
 codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `len`,<Length trace>,Parameter `len`,Array declaration,Array access: Offset: [3⋅len + 1, 3⋅len + 1] Size: [3⋅len + 1, 3⋅len + 1]]
-codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 20 Size: 10]
+codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `y.f[*]`,<Length trace>,Array declaration,Array access: Offset: [min(20, y.f[*]), max(20, y.f[*])] Size: 10]
 codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `x->f[*]`,Assignment,Assignment,Assignment,Array access: Offset: -1 Size: 2]
 codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
 codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 3 Size: 3]
 codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 6 Size: 6]
 codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr5_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr6_Bad, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
+codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr6_Good_FP, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 10]
 codetoanalyze/c/bufferoverrun/big_array.c, use_big_array_bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Call,Array declaration,Assignment,Assignment,Array access: Offset: 999999999 Size: 26460]
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]

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

@@ -38,7 +38,6 @@ codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empt
 codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [1, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: -1 Size: 10]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]
-codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: [-oo, +oo] Size: 5]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_flexible_array_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 7 Size: 5]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]
@@ -80,7 +79,7 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5,
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 4 Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,<Length trace>,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Array declaration,Assignment,Assignment,Array access: Offset: [-oo, +oo] Size: 5]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,<RHS trace>,Parameter `__n`,Binary operation: ([3, +oo] + 42):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [45, +oo]):unsigned64]

infer/tests/codetoanalyze/cpp/bufferoverrun/realloc.cpp

@@ -20,7 +20,7 @@ void realloc_Bad() {
   buf2[buf2[0]] = 0;
 }
 
-void realloc_Good_FP() {
+void realloc2_Good() {
   int* buf1 = (int*)malloc(2 * sizeof(int));
   for (int i = 0; i < 2; i++) {
     buf1[i] = 3;