[inferbo] Separate offset and index in condition

Summary:
This diff preserves values of offset and index separately, rather than
one value of their addition, because premature addition results in
imprecise FPs by the limited expressiveness of the domain.

Reviewed By: mbouaziz

Differential Revision: D10851393

fbshipit-source-id: 1685ead36

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -99,91 +99,106 @@ end
 
 module ArrayAccessCondition = struct
   type t =
-    { idx: ItvPure.astate
+    { offset: ItvPure.astate
+    ; idx: ItvPure.astate
     ; size: ItvPure.astate
     ; idx_sym_exp: Relation.SymExp.t option
     ; size_sym_exp: Relation.SymExp.t option
     ; relation: Relation.astate }
   [@@deriving compare]
 
-  let get_symbols c = ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size
+  let get_symbols c =
-
+    ItvPure.get_symbols c.offset @ ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size
-  let set_size_pos : t -> t =
-   fun c ->
-    let size' = ItvPure.make_positive c.size in
-    if phys_equal size' c.size then c else {c with size= size'}
 
 
   let pp : F.formatter -> t -> unit =
    fun fmt c ->
-    let c = set_size_pos c in
+    let pp_offset fmt =
-    F.fprintf fmt "%a < %a" ItvPure.pp c.idx ItvPure.pp c.size ;
+      if not (ItvPure.is_zero c.offset) then F.fprintf fmt "%a + " ItvPure.pp c.offset
+    in
+    F.fprintf fmt "%t%a < %a" pp_offset ItvPure.pp c.idx ItvPure.pp (ItvPure.make_positive c.size) ;
     if Option.is_some Config.bo_relational_domain then
       F.fprintf fmt "@,%a < %a when %a" Relation.SymExp.pp_opt c.idx_sym_exp Relation.SymExp.pp_opt
         c.size_sym_exp Relation.pp c.relation
 
 
+  (* TODO: change description to distinguish offset and index *)
   let pp_description : F.formatter -> t -> unit =
    fun fmt c ->
-    let c = set_size_pos c in
+    F.fprintf fmt "Offset: %a Size: %a" ItvPure.pp (ItvPure.plus c.offset c.idx) ItvPure.pp
-    F.fprintf fmt "Offset: %a Size: %a" ItvPure.pp c.idx ItvPure.pp c.size
+      (ItvPure.make_positive c.size)
 
 
   let make :
-         idx:ItvPure.t
+         offset:ItvPure.t
+      -> idx:ItvPure.t
       -> size:ItvPure.t
       -> idx_sym_exp:Relation.SymExp.t option
       -> size_sym_exp:Relation.SymExp.t option
       -> relation:Relation.astate
       -> t option =
-   fun ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation ->
+   fun ~offset ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation ->
-    if ItvPure.is_invalid idx || ItvPure.is_invalid size then None
+    if ItvPure.is_invalid offset || ItvPure.is_invalid idx || ItvPure.is_invalid size then None
-    else Some {idx; size; idx_sym_exp; size_sym_exp; relation}
+    else Some {offset; idx; size; idx_sym_exp; size_sym_exp; relation}
+
 
+  let have_similar_bounds {offset= loff; idx= lidx; size= lsiz}
+      {offset= roff; idx= ridx; size= rsiz} =
+    ItvPure.have_similar_bounds loff roff
+    && ItvPure.have_similar_bounds lidx ridx
+    && ItvPure.have_similar_bounds lsiz rsiz
 
-  let have_similar_bounds {idx= lidx; size= lsiz} {idx= ridx; size= rsiz} =
-    ItvPure.have_similar_bounds lidx ridx && ItvPure.have_similar_bounds lsiz rsiz
 
+  let has_infty {offset; idx; size} =
+    ItvPure.has_infty offset || ItvPure.has_infty idx || ItvPure.has_infty size
 
-  let has_infty {idx; size} = ItvPure.has_infty idx || ItvPure.has_infty size
 
-  let xcompare ~lhs:{idx= lidx; size= lsiz} ~rhs:{idx= ridx; size= rsiz} =
+  let xcompare ~lhs:{offset= loff; idx= lidx; size= lsiz} ~rhs:{offset= roff; idx= ridx; size= rsiz}
+      =
+    let offcmp = ItvPure.xcompare ~lhs:loff ~rhs:roff in
     let idxcmp = ItvPure.xcompare ~lhs:lidx ~rhs:ridx in
     let sizcmp = ItvPure.xcompare ~lhs:lsiz ~rhs:rsiz in
-    match (idxcmp, sizcmp) with
+    match (offcmp, idxcmp, sizcmp) with
-    | `Equal, `Equal ->
+    | `Equal, `Equal, `Equal ->
         `Equal
-    | `NotComparable, _ ->
+    | `NotComparable, _, _ | _, `NotComparable, _ ->
         `NotComparable
-    | `Equal, (`LeftSmallerThanRight | `LeftSubsumesRight) ->
+    | `Equal, `Equal, (`LeftSmallerThanRight | `LeftSubsumesRight) ->
         `LeftSubsumesRight
-    | `Equal, (`RightSmallerThanLeft | `RightSubsumesLeft) ->
+    | `Equal, `Equal, (`RightSmallerThanLeft | `RightSubsumesLeft) ->
         `RightSubsumesLeft
-    | `LeftSubsumesRight, (`Equal | `LeftSubsumesRight) ->
+    | (`Equal | `LeftSubsumesRight), (`Equal | `LeftSubsumesRight), (`Equal | `LeftSubsumesRight)
+      ->
         `LeftSubsumesRight
-    | `RightSubsumesLeft, (`Equal | `RightSubsumesLeft) ->
+    | (`Equal | `RightSubsumesLeft), (`Equal | `RightSubsumesLeft), (`Equal | `RightSubsumesLeft)
+      ->
         `RightSubsumesLeft
-    | (`LeftSmallerThanRight | `RightSmallerThanLeft), _ ->
+    | (`Equal | `LeftSmallerThanRight), (`Equal | `LeftSmallerThanRight), _
-        let lidxpos = ItvPure.le_sem ItvPure.zero lidx in
+    | (`Equal | `RightSmallerThanLeft), (`Equal | `RightSmallerThanLeft), _ ->
-        let ridxpos = ItvPure.le_sem ItvPure.zero ridx in
+        let lidxpos = ItvPure.le_sem (ItvPure.neg lidx) loff in
+        let ridxpos = ItvPure.le_sem (ItvPure.neg ridx) roff in
         if not (Itv.Boolean.equal lidxpos ridxpos) then `NotComparable
         else if Itv.Boolean.is_true lidxpos then
           (* both idx >= 0 *)
-          match (idxcmp, sizcmp) with
+          match (offcmp, idxcmp, sizcmp) with
-          | `LeftSmallerThanRight, (`Equal | `RightSmallerThanLeft | `RightSubsumesLeft) ->
+          | ( (`Equal | `LeftSmallerThanRight)
+            , (`Equal | `LeftSmallerThanRight)
+            , (`Equal | `RightSmallerThanLeft | `RightSubsumesLeft) ) ->
               `RightSubsumesLeft
-          | `RightSmallerThanLeft, (`Equal | `LeftSmallerThanRight | `LeftSubsumesRight) ->
+          | ( (`Equal | `RightSmallerThanLeft)
+            , (`Equal | `RightSmallerThanLeft)
+            , (`Equal | `LeftSmallerThanRight | `LeftSubsumesRight) ) ->
               `LeftSubsumesRight
           | _ ->
               `NotComparable
         else if Itv.Boolean.is_false lidxpos then
           (* both idx < 0, size doesn't matter *)
-          match idxcmp with
+          match (offcmp, idxcmp) with
-          | `LeftSmallerThanRight ->
+          | `Equal, `LeftSmallerThanRight | `LeftSmallerThanRight, `Equal ->
               `LeftSubsumesRight
-          | `RightSmallerThanLeft ->
+          | `Equal, `RightSmallerThanLeft | `RightSmallerThanLeft, `Equal ->
               `RightSubsumesLeft
-          | `Equal ->
+          | `Equal, `Equal ->
               `Equal
           | _ ->
               `NotComparable
@@ -192,34 +207,34 @@ module ArrayAccessCondition = struct
         `NotComparable
 
 
-  let filter1 : t -> bool =
+  let filter1 : real_idx:ItvPure.t -> t -> bool =
-   fun c ->
+   fun ~real_idx c ->
-    ItvPure.is_top c.idx || ItvPure.is_top c.size || ItvPure.is_lb_infty c.idx
+    ItvPure.is_top real_idx || ItvPure.is_top c.size || ItvPure.is_lb_infty real_idx
     || ItvPure.is_lb_infty c.size
-    || (ItvPure.is_nat c.idx && ItvPure.is_nat c.size)
+    || (ItvPure.is_nat real_idx && ItvPure.is_nat c.size)
 
 
-  let filter2 : t -> bool =
+  let filter2 : real_idx:ItvPure.t -> t -> bool =
-   fun c ->
+   fun ~real_idx c ->
     (* basically, alarms involving infinity are filtered *)
-    ((not (ItvPure.is_finite c.idx)) || not (ItvPure.is_finite c.size))
+    ((not (ItvPure.is_finite real_idx)) || not (ItvPure.is_finite c.size))
     && (* except the following cases *)
        not
-         ( Bound.is_not_infty (ItvPure.lb c.idx)
+         ( Bound.is_not_infty (ItvPure.lb real_idx)
            && (* idx non-infty lb < 0 *)
-              Bound.lt (ItvPure.lb c.idx) Bound.zero
+              Bound.lt (ItvPure.lb real_idx) Bound.zero
-         || Bound.is_not_infty (ItvPure.lb c.idx)
+         || Bound.is_not_infty (ItvPure.lb real_idx)
             && (* idx non-infty lb > size lb *)
-               Bound.gt (ItvPure.lb c.idx) (ItvPure.lb c.size)
+               Bound.gt (ItvPure.lb real_idx) (ItvPure.lb c.size)
-         || Bound.is_not_infty (ItvPure.lb c.idx)
+         || Bound.is_not_infty (ItvPure.lb real_idx)
             && (* idx non-infty lb > size ub *)
-               Bound.gt (ItvPure.lb c.idx) (ItvPure.ub c.size)
+               Bound.gt (ItvPure.lb real_idx) (ItvPure.ub c.size)
-         || Bound.is_not_infty (ItvPure.ub c.idx)
+         || Bound.is_not_infty (ItvPure.ub real_idx)
             && (* idx non-infty ub > size lb *)
-               Bound.gt (ItvPure.ub c.idx) (ItvPure.lb c.size)
+               Bound.gt (ItvPure.ub real_idx) (ItvPure.lb c.size)
-         || Bound.is_not_infty (ItvPure.ub c.idx)
+         || Bound.is_not_infty (ItvPure.ub real_idx)
             && (* idx non-infty ub > size ub *)
-               Bound.gt (ItvPure.ub c.idx) (ItvPure.ub c.size) )
+               Bound.gt (ItvPure.ub real_idx) (ItvPure.ub c.size) )
 
 
   (* check buffer overrun and return its confidence *)
@@ -228,17 +243,18 @@ module ArrayAccessCondition = struct
     (* idx = [il, iu], size = [sl, su],
        For arrays : we want to check that 0 <= idx < size
        For adding into arraylists: we want to check that 0 <= idx <= size *)
-    let c' = set_size_pos c in
+    let real_idx = ItvPure.plus c.offset c.idx in
+    let size = ItvPure.make_positive c.size in
     (* if sl < 0, use sl' = 0 *)
     let not_overrun =
-      if is_collection_add then ItvPure.le_sem c'.idx c'.size
+      if is_collection_add then ItvPure.le_sem real_idx size
-      else if Relation.lt_sat_opt c'.idx_sym_exp c'.size_sym_exp c'.relation then Itv.Boolean.true_
+      else if Relation.lt_sat_opt c.idx_sym_exp c.size_sym_exp c.relation then Itv.Boolean.true_
-      else ItvPure.lt_sem c'.idx c'.size
+      else ItvPure.lt_sem real_idx size
     in
     let not_underrun =
-      if Relation.le_sat_opt (Some Relation.SymExp.zero) c'.idx_sym_exp c'.relation then
+      if Relation.le_sat_opt (Some Relation.SymExp.zero) c.idx_sym_exp c.relation then
         Itv.Boolean.true_
-      else ItvPure.le_sem ItvPure.zero c'.idx
+      else ItvPure.le_sem ItvPure.zero real_idx
     in
     (* il >= 0 and iu < sl, definitely not an error *)
     if Itv.Boolean.is_true not_overrun && Itv.Boolean.is_true not_underrun then
@@ -247,19 +263,21 @@ module ArrayAccessCondition = struct
       {report_issue_type= Some IssueType.buffer_overrun_l1; propagate= false}
       (* su <= iu < +oo, most probably an error *)
     else if
-      Bound.is_not_infty (ItvPure.ub c.idx) && Bound.le (ItvPure.ub c.size) (ItvPure.ub c.idx)
+      Bound.is_not_infty (ItvPure.ub real_idx) && Bound.le (ItvPure.ub size) (ItvPure.ub real_idx)
     then {report_issue_type= Some IssueType.buffer_overrun_l2; propagate= false}
       (* symbolic il >= sl, probably an error *)
     else if
-      Bound.is_symbolic (ItvPure.lb c.idx) && Bound.le (ItvPure.lb c'.size) (ItvPure.lb c.idx)
+      Bound.is_symbolic (ItvPure.lb real_idx) && Bound.le (ItvPure.lb size) (ItvPure.lb real_idx)
     then {report_issue_type= Some IssueType.buffer_overrun_s2; propagate= true}
     else
       (* other symbolic bounds are probably too noisy *)
-      let is_symbolic = ItvPure.is_symbolic c.idx || ItvPure.is_symbolic c.size in
+      let is_symbolic =
+        ItvPure.is_symbolic c.offset || ItvPure.is_symbolic c.idx || ItvPure.is_symbolic size
+      in
       let report_issue_type =
         if Config.bo_debug <= 3 && is_symbolic then None
-        else if filter1 c then Some IssueType.buffer_overrun_l5
+        else if filter1 ~real_idx c then Some IssueType.buffer_overrun_l5
-        else if filter2 c then Some IssueType.buffer_overrun_l4
+        else if filter2 ~real_idx c then Some IssueType.buffer_overrun_l4
         else Some IssueType.buffer_overrun_l3
       in
       {report_issue_type; propagate= is_symbolic}
@@ -272,12 +290,14 @@ module ArrayAccessCondition = struct
       -> t
       -> t option =
    fun eval_sym rel_map caller_relation c ->
-    match (ItvPure.subst c.idx eval_sym, ItvPure.subst c.size eval_sym) with
+    match
-    | NonBottom idx, NonBottom size ->
+      (ItvPure.subst c.offset eval_sym, ItvPure.subst c.idx eval_sym, ItvPure.subst c.size eval_sym)
+    with
+    | NonBottom offset, NonBottom idx, NonBottom size ->
         let idx_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.idx_sym_exp in
         let size_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.size_sym_exp in
         let relation = Relation.instantiate rel_map ~caller:caller_relation ~callee:c.relation in
-        Some {idx; size; idx_sym_exp; size_sym_exp; relation}
+        Some {offset; idx; size; idx_sym_exp; size_sym_exp; relation}
     | _ ->
         None
 
@@ -780,9 +800,9 @@ module ConditionSet = struct
         join [cwt] condset
 
 
-  let add_array_access location ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp ~relation
+  let add_array_access location ~offset ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp
-      val_traces condset =
+      ~relation val_traces condset =
-    ArrayAccessCondition.make ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation
+    ArrayAccessCondition.make ~offset ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation
     |> Condition.make_array_access ~is_collection_add
     |> add_opt location val_traces condset
 

infer/src/bufferoverrun/bufferOverrunProofObligations.mli

@@ -36,6 +36,7 @@ module ConditionSet : sig
 
   val add_array_access :
        Location.t
+    -> offset:ItvPure.astate
     -> idx:ItvPure.astate
     -> size:ItvPure.astate
     -> is_collection_add:bool

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -297,12 +297,20 @@ end
 module Check = struct
   let check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces
       ?(is_collection_add = false) location cond_set =
-    let arr_traces = Dom.Val.get_traces arr in
     match (size, idx) with
     | NonBottom length, NonBottom idx ->
+        let offset =
+          match ArrayBlk.offsetof (Dom.Val.get_array_blk arr) with
+          | Bottom ->
+              (* Java's collection has no offset. *)
+              Itv.ItvPure.zero
+          | NonBottom offset ->
+              offset
+        in
+        let arr_traces = Dom.Val.get_traces arr in
         let traces = TraceSet.merge ~arr_traces ~idx_traces location in
-        PO.ConditionSet.add_array_access location ~size:length ~idx ~size_sym_exp ~idx_sym_exp
+        PO.ConditionSet.add_array_access location ~size:length ~offset ~idx ~size_sym_exp
-          ~relation ~is_collection_add traces cond_set
+          ~idx_sym_exp ~relation ~is_collection_add traces cond_set
     | _ ->
         cond_set
 
@@ -311,20 +319,19 @@ module Check = struct
     let arr_blk = Dom.Val.get_array_blk arr in
     let size = ArrayBlk.sizeof arr_blk in
     let size_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_size_sym arr) in
-    let offset = ArrayBlk.offsetof arr_blk in
-    let offset_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_offset_sym arr) in
     let idx_itv = Dom.Val.get_itv idx in
     let idx_traces = Dom.Val.get_traces idx in
-    let idx_in_blk = (if is_plus then Itv.plus else Itv.minus) offset idx_itv in
+    let idx = if is_plus then idx_itv else Itv.neg idx_itv in
     let idx_sym_exp =
+      let offset_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_offset_sym arr) in
       Option.map2 offset_sym_exp idx_sym_exp ~f:(fun offset_sym_exp idx_sym_exp ->
           let op = if is_plus then Relation.SymExp.plus else Relation.SymExp.minus in
           op idx_sym_exp offset_sym_exp )
     in
     L.(debug BufferOverrun Verbose)
-      "@[<v 2>Add condition :@,array: %a@,  idx: %a@,@]@." ArrayBlk.pp arr_blk Itv.pp idx_in_blk ;
+      "@[<v 2>Add condition :@,array: %a@,  idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp
-    check_access ~size ~idx:idx_in_blk ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces
+      (ArrayBlk.offsetof arr_blk) Itv.pp idx ;
-      location cond_set
+    check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces location cond_set
 
 
   let collection_access ~array_exp ~index_exp ?(is_collection_add = false) mem location cond_set =
@@ -349,14 +356,14 @@ module Check = struct
   let array_access_byte ~arr ~idx ~relation ~is_plus location cond_set =
     let arr_blk = Dom.Val.get_array_blk arr in
     let size = ArrayBlk.sizeof_byte arr_blk in
-    let offset = ArrayBlk.offsetof arr_blk in
     let idx_itv = Dom.Val.get_itv idx in
     let idx_traces = Dom.Val.get_traces idx in
-    let idx_in_blk = (if is_plus then Itv.plus else Itv.minus) offset idx_itv in
+    let idx = if is_plus then idx_itv else Itv.neg idx_itv in
     L.(debug BufferOverrun Verbose)
-      "@[<v 2>Add condition :@,array: %a@,  idx: %a@,@]@." ArrayBlk.pp arr_blk Itv.pp idx_in_blk ;
+      "@[<v 2>Add condition :@,array: %a@,  idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp
-    check_access ~size ~idx:idx_in_blk ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr
+      (ArrayBlk.offsetof arr_blk) Itv.pp idx ;
-      ~idx_traces location cond_set ~is_collection_add:true
+    check_access ~size ~idx ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr ~idx_traces
+      location cond_set ~is_collection_add:true
 
 
   let lindex_byte ~array_exp ~byte_index_exp mem location cond_set =

infer/src/bufferoverrun/itv.mli

@@ -98,6 +98,8 @@ module ItvPure : sig
 
   val is_top : t -> bool
 
+  val is_zero : t -> bool
+
   val is_one : t -> bool
 
   val is_ge_zero : t -> bool
@@ -136,6 +138,8 @@ module ItvPure : sig
 
   val subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted
 
+  val neg : t -> t
+
   val plus : t -> t -> t
 
   val minus : t -> t -> t

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

@@ -48,7 +48,7 @@ int array_min_index_from_one_FP(int* a, int length) {
   We need a either a narrowing or a relational domain to prove that
   index_min < length
 */
-void call_array_min_index_from_one_good_FP() {
+void call_array_min_index_from_one_good() {
   int a[2];
   a[array_min_index_from_one_FP(a, 2) - 1] = 0;
 }

infer/tests/codetoanalyze/c/bufferoverrun/do_while.c

@@ -17,8 +17,12 @@ void do_while_sub(char* a, int len) {
   } while (i < len);
 }
 
-void do_while() {
+void do_while_Good() {
   char* a = malloc(10);
   do_while_sub(a, 10); /* SAFE */
+}
+
+void do_while_Bad() {
+  char* a = malloc(10);
   do_while_sub(a, 11); /* BUG */
 }

infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c

@@ -80,3 +80,19 @@ void malloc_sizeof_value_leak_good() {
   }
   /* missing free(x) */
 }
+
+void initialize_arr(int* arr, int count) {
+  for (int i = 0; i < count; ++i) {
+    arr[i] = 0;
+  }
+}
+
+void call_initialize_arr_Good() {
+  int arr[10];
+  initialize_arr(arr, 5);
+}
+
+void call_initialize_arr_Bad() {
+  int arr[10];
+  initialize_arr(arr, 20);
+}

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

@@ -20,7 +20,6 @@ codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2
 codetoanalyze/c/bufferoverrun/arith.c, plus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: unknown_int,Assignment,Binop: ([-oo, 9223372036854775807] + 1):signed64]
 codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
-codetoanalyze/c/bufferoverrun/array_content.c, call_array_min_index_from_one_good_FP, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: a,Assignment,ArrayAccess: Offset: [1, +oo] Size: 2 by call to `array_min_index_from_one_FP` ]
 codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
@@ -40,13 +39,14 @@ codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Bad_FN, 4, CONDITI
 codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
-codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: a,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10 by call to `do_while_sub` ]
+codetoanalyze/c/bufferoverrun/do_while.c, do_while_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: a,Assignment,ArrayAccess: Offset: [0, 10] Size: 10 by call to `do_while_sub` ]
 codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,ArrayAccess: Offset: 1 Size: 1 by call to `two_accesses` ]
 codetoanalyze/c/bufferoverrun/duplicates.c, tsa_one_alarm_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: 3 Size: 1 by call to `two_symbolic_accesses` ]
 codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: -1 Size: 1 by call to `two_symbolic_accesses` ]
 codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: 1 Size: 1 by call to `two_symbolic_accesses` ]
 codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 30 Size: 10]
+codetoanalyze/c/bufferoverrun/for_loop.c, call_initialize_arr_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,Assignment,ArrayAccess: Offset: [0, 19] Size: 10 by call to `initialize_arr` ]
 codetoanalyze/c/bufferoverrun/for_loop.c, call_two_loops_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: m,Assignment,Return,ArrayAccess: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [0, 9] Size: [5, 10]]
 codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10]

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -126,7 +126,7 @@ codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.
 codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addKeyToMap(java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonString.java, libraries.marauder.analytics.utils.json.JsonString.<init>(java.lang.String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
-codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: char[] String.toCharArray(),Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: char[] String.toCharArray(),Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.String):java.lang.StringBuilder, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []