diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index eb53761a7..cd67ea4cb 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/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 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 get_symbols c = + ItvPure.get_symbols c.offset @ ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size let pp : F.formatter -> t -> unit = fun fmt c -> - let c = set_size_pos c in - F.fprintf fmt "%a < %a" ItvPure.pp c.idx ItvPure.pp c.size ; + let pp_offset fmt = + 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 c.idx ItvPure.pp c.size + F.fprintf fmt "Offset: %a Size: %a" ItvPure.pp (ItvPure.plus c.offset c.idx) ItvPure.pp + (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 -> - if ItvPure.is_invalid idx || ItvPure.is_invalid size then None - else Some {idx; size; idx_sym_exp; size_sym_exp; relation} + fun ~offset ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation -> + if ItvPure.is_invalid offset || ItvPure.is_invalid idx || ItvPure.is_invalid size then None + 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 - | `Equal, `Equal -> + match (offcmp, idxcmp, sizcmp) with + | `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), _ -> - let lidxpos = ItvPure.le_sem ItvPure.zero lidx in - let ridxpos = ItvPure.le_sem ItvPure.zero ridx in + | (`Equal | `LeftSmallerThanRight), (`Equal | `LeftSmallerThanRight), _ + | (`Equal | `RightSmallerThanLeft), (`Equal | `RightSmallerThanLeft), _ -> + 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 - | `LeftSmallerThanRight, (`Equal | `RightSmallerThanLeft | `RightSubsumesLeft) -> + match (offcmp, idxcmp, sizcmp) with + | ( (`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 - | `LeftSmallerThanRight -> + match (offcmp, idxcmp) with + | `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 = - fun c -> - ItvPure.is_top c.idx || ItvPure.is_top c.size || ItvPure.is_lb_infty c.idx + let filter1 : real_idx:ItvPure.t -> t -> bool = + fun ~real_idx c -> + 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 = - fun c -> + let filter2 : real_idx:ItvPure.t -> t -> bool = + 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.is_not_infty (ItvPure.lb c.idx) + Bound.lt (ItvPure.lb real_idx) Bound.zero + || 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.is_not_infty (ItvPure.lb c.idx) + Bound.gt (ItvPure.lb real_idx) (ItvPure.lb c.size) + || 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.is_not_infty (ItvPure.ub c.idx) + Bound.gt (ItvPure.lb real_idx) (ItvPure.ub c.size) + || 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.is_not_infty (ItvPure.ub c.idx) + Bound.gt (ItvPure.ub real_idx) (ItvPure.lb c.size) + || 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 - 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 + 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 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 filter2 c then Some IssueType.buffer_overrun_l4 + else if filter1 ~real_idx c then Some IssueType.buffer_overrun_l5 + 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 - | NonBottom idx, NonBottom size -> + match + (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 - val_traces condset = - ArrayAccessCondition.make ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation + let add_array_access location ~offset ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp + ~relation val_traces condset = + 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 diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 1cc97f799..0e4d02151 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 454273eab..ab28cee1d 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/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 - ~relation ~is_collection_add traces cond_set + PO.ConditionSet.add_array_access location ~size:length ~offset ~idx ~size_sym_exp + ~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) - "@[Add condition :@,array: %a@, idx: %a@,@]@." ArrayBlk.pp arr_blk Itv.pp idx_in_blk ; - check_access ~size ~idx:idx_in_blk ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces - location cond_set + "@[Add condition :@,array: %a@, idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp + (ArrayBlk.offsetof arr_blk) Itv.pp idx ; + 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) - "@[Add condition :@,array: %a@, idx: %a@,@]@." ArrayBlk.pp arr_blk Itv.pp idx_in_blk ; - check_access ~size ~idx:idx_in_blk ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr - ~idx_traces location cond_set ~is_collection_add:true + "@[Add condition :@,array: %a@, idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp + (ArrayBlk.offsetof arr_blk) Itv.pp idx ; + 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 = diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index b53599db6..ecb697e3e 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c b/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c index ea96a5c77..03f6df90a 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c +++ b/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; } diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/do_while.c b/infer/tests/codetoanalyze/c/bufferoverrun/do_while.c index 3ee10eaea..fe1b5e0e7 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/do_while.c +++ b/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 */ } diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c b/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c index c9b747755..02be909e5 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c +++ b/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); +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 61dddd5b5..4dfa06150 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/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] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index da829f660..ff55c48e9 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/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.(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, []