From e190325b8280ac519a5b251ab6c293af5220b3c5 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 16 Nov 2018 21:34:59 -0800 Subject: [PATCH] [inferbo] Distinguish collection add against array access in pp Reviewed By: mbouaziz Differential Revision: D13096380 fbshipit-source-id: d8878749f --- .../bufferOverrunProofObligations.ml | 180 +++++++++--------- .../codetoanalyze/c/bufferoverrun/issues.exp | 34 ++-- .../codetoanalyze/java/performance/issues.exp | 8 +- 3 files changed, 115 insertions(+), 107 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index a7f2be62e..b9c7ab332 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -102,6 +102,7 @@ module ArrayAccessCondition = struct { offset: ItvPure.astate ; idx: ItvPure.astate ; size: ItvPure.astate + ; is_collection_add: bool ; idx_sym_exp: Relation.SymExp.t option ; size_sym_exp: Relation.SymExp.t option ; relation: Relation.astate } @@ -117,10 +118,12 @@ module ArrayAccessCondition = struct 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) ; + let cmp = if c.is_collection_add then "<=" else "<" in + F.fprintf fmt "%t%a %s %a" pp_offset ItvPure.pp c.idx cmp 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 + F.fprintf fmt "@,%a %s %a when %a" Relation.SymExp.pp_opt c.idx_sym_exp cmp + Relation.SymExp.pp_opt c.size_sym_exp Relation.pp c.relation let pp_description : F.formatter -> t -> unit = @@ -132,25 +135,29 @@ module ArrayAccessCondition = struct F.fprintf fmt "%a (= %a + %a)" ItvPure.pp (ItvPure.plus c.offset c.idx) ItvPure.pp c.offset ItvPure.pp c.idx in - F.fprintf fmt "Offset: %t Size: %a" pp_offset ItvPure.pp (ItvPure.make_positive c.size) + F.fprintf fmt "Offset%s: %t Size: %a" + (if c.is_collection_add then " added" else "") + pp_offset ItvPure.pp (ItvPure.make_positive c.size) let make : offset:ItvPure.t -> idx:ItvPure.t -> size:ItvPure.t + -> is_collection_add:bool -> idx_sym_exp:Relation.SymExp.t option -> size_sym_exp:Relation.SymExp.t option -> relation:Relation.astate -> t option = - fun ~offset ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation -> + fun ~offset ~idx ~size ~is_collection_add ~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} + else Some {offset; idx; size; is_collection_add; 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 + let have_similar_bounds {offset= loff; idx= lidx; size= lsiz; is_collection_add= lcol} + {offset= roff; idx= ridx; size= rsiz; is_collection_add= rcol} = + Bool.equal lcol rcol + && ItvPure.have_similar_bounds loff roff && ItvPure.have_similar_bounds lidx ridx && ItvPure.have_similar_bounds lsiz rsiz @@ -159,58 +166,60 @@ module ArrayAccessCondition = struct ItvPure.has_infty offset || ItvPure.has_infty idx || ItvPure.has_infty size - 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 (offcmp, idxcmp, sizcmp) with - | `Equal, `Equal, `Equal -> - `Equal - | `NotComparable, _, _ | _, `NotComparable, _ -> - `NotComparable - | `Equal, `Equal, (`LeftSmallerThanRight | `LeftSubsumesRight) -> - `LeftSubsumesRight - | `Equal, `Equal, (`RightSmallerThanLeft | `RightSubsumesLeft) -> - `RightSubsumesLeft - | (`Equal | `LeftSubsumesRight), (`Equal | `LeftSubsumesRight), (`Equal | `LeftSubsumesRight) - -> - `LeftSubsumesRight - | (`Equal | `RightSubsumesLeft), (`Equal | `RightSubsumesLeft), (`Equal | `RightSubsumesLeft) - -> - `RightSubsumesLeft - | (`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 (offcmp, idxcmp, sizcmp) with - | ( (`Equal | `LeftSmallerThanRight) - , (`Equal | `LeftSmallerThanRight) - , (`Equal | `RightSmallerThanLeft | `RightSubsumesLeft) ) -> - `RightSubsumesLeft - | ( (`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 (offcmp, idxcmp) with - | `Equal, `LeftSmallerThanRight | `LeftSmallerThanRight, `Equal -> - `LeftSubsumesRight - | `Equal, `RightSmallerThanLeft | `RightSmallerThanLeft, `Equal -> - `RightSubsumesLeft - | `Equal, `Equal -> - `Equal - | _ -> - `NotComparable - else `NotComparable - | _ -> - `NotComparable + let xcompare ~lhs:{offset= loff; idx= lidx; size= lsiz; is_collection_add= lcol} + ~rhs:{offset= roff; idx= ridx; size= rsiz; is_collection_add= rcol} = + if not (Bool.equal lcol rcol) then `NotComparable + else + 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 (offcmp, idxcmp, sizcmp) with + | `Equal, `Equal, `Equal -> + `Equal + | `NotComparable, _, _ | _, `NotComparable, _ -> + `NotComparable + | `Equal, `Equal, (`LeftSmallerThanRight | `LeftSubsumesRight) -> + `LeftSubsumesRight + | `Equal, `Equal, (`RightSmallerThanLeft | `RightSubsumesLeft) -> + `RightSubsumesLeft + | (`Equal | `LeftSubsumesRight), (`Equal | `LeftSubsumesRight), (`Equal | `LeftSubsumesRight) + -> + `LeftSubsumesRight + | (`Equal | `RightSubsumesLeft), (`Equal | `RightSubsumesLeft), (`Equal | `RightSubsumesLeft) + -> + `RightSubsumesLeft + | (`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 (offcmp, idxcmp, sizcmp) with + | ( (`Equal | `LeftSmallerThanRight) + , (`Equal | `LeftSmallerThanRight) + , (`Equal | `RightSmallerThanLeft | `RightSubsumesLeft) ) -> + `RightSubsumesLeft + | ( (`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 (offcmp, idxcmp) with + | `Equal, `LeftSmallerThanRight | `LeftSmallerThanRight, `Equal -> + `LeftSubsumesRight + | `Equal, `RightSmallerThanLeft | `RightSmallerThanLeft, `Equal -> + `RightSubsumesLeft + | `Equal, `Equal -> + `Equal + | _ -> + `NotComparable + else `NotComparable + | _ -> + `NotComparable let filter1 : real_idx:ItvPure.t -> t -> bool = @@ -244,13 +253,15 @@ module ArrayAccessCondition = struct (* check buffer overrun and return its confidence *) - let check : is_collection_add:bool -> t -> checked_condition = - fun ~is_collection_add c -> + let check : t -> checked_condition = + fun c -> (* 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 *) + For adding into collections : we want to check that 0 <= idx <= size *) let real_idx = ItvPure.plus c.offset c.idx in - let size = ItvPure.make_positive (if is_collection_add then ItvPure.succ c.size else c.size) in + let size = + ItvPure.make_positive (if c.is_collection_add then ItvPure.succ c.size else c.size) + in (* if sl < 0, use sl' = 0 *) let not_overrun = if Relation.lt_sat_opt c.idx_sym_exp c.size_sym_exp c.relation then Itv.Boolean.true_ @@ -297,7 +308,7 @@ module ArrayAccessCondition = struct 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 {offset; idx; size; idx_sym_exp; size_sym_exp; relation} + Some {c with offset; idx; size; idx_sym_exp; size_sym_exp; relation} | _ -> None @@ -469,21 +480,19 @@ end module Condition = struct type t = | AllocSize of AllocSizeCondition.t - | ArrayAccess of {is_collection_add: bool; c: ArrayAccessCondition.t} + | ArrayAccess of ArrayAccessCondition.t | BinaryOperation of BinaryOperationCondition.t let make_alloc_size = Option.map ~f:(fun c -> AllocSize c) - let make_array_access ~is_collection_add = - Option.map ~f:(fun c -> ArrayAccess {is_collection_add; c}) - + let make_array_access = Option.map ~f:(fun c -> ArrayAccess c) let make_binary_operation = Option.map ~f:(fun c -> BinaryOperation c) let get_symbols = function | AllocSize c -> AllocSizeCondition.get_symbols c - | ArrayAccess {c} -> + | ArrayAccess c -> ArrayAccessCondition.get_symbols c | BinaryOperation c -> BinaryOperationCondition.get_symbols c @@ -492,9 +501,8 @@ module Condition = struct let subst eval_sym rel_map caller_relation = function | AllocSize c -> AllocSizeCondition.subst eval_sym c |> make_alloc_size - | ArrayAccess {is_collection_add; c} -> - ArrayAccessCondition.subst eval_sym rel_map caller_relation c - |> make_array_access ~is_collection_add + | ArrayAccess c -> + ArrayAccessCondition.subst eval_sym rel_map caller_relation c |> make_array_access | BinaryOperation c -> BinaryOperationCondition.subst eval_sym c |> make_binary_operation @@ -503,7 +511,7 @@ module Condition = struct match (c1, c2) with | AllocSize c1, AllocSize c2 -> AllocSizeCondition.have_similar_bounds c1 c2 - | ArrayAccess {c= c1}, ArrayAccess {c= c2} -> + | ArrayAccess c1, ArrayAccess c2 -> ArrayAccessCondition.have_similar_bounds c1 c2 | BinaryOperation c1, BinaryOperation c2 -> BinaryOperationCondition.have_similar_bounds c1 c2 @@ -512,7 +520,7 @@ module Condition = struct let has_infty = function - | ArrayAccess {c} -> + | ArrayAccess c -> ArrayAccessCondition.has_infty c | BinaryOperation c -> BinaryOperationCondition.has_infty c @@ -524,8 +532,7 @@ module Condition = struct match (lhs, rhs) with | AllocSize lhs, AllocSize rhs -> AllocSizeCondition.xcompare ~lhs ~rhs - | ArrayAccess {is_collection_add= b1; c= lhs}, ArrayAccess {is_collection_add= b2; c= rhs} - when Bool.equal b1 b2 -> + | ArrayAccess lhs, ArrayAccess rhs -> ArrayAccessCondition.xcompare ~lhs ~rhs | BinaryOperation lhs, BinaryOperation rhs -> BinaryOperationCondition.xcompare ~lhs ~rhs @@ -536,7 +543,7 @@ module Condition = struct let pp fmt = function | AllocSize c -> AllocSizeCondition.pp fmt c - | ArrayAccess {c} -> + | ArrayAccess c -> ArrayAccessCondition.pp fmt c | BinaryOperation c -> BinaryOperationCondition.pp fmt c @@ -545,7 +552,7 @@ module Condition = struct let pp_description fmt = function | AllocSize c -> AllocSizeCondition.pp_description fmt c - | ArrayAccess {c} -> + | ArrayAccess c -> ArrayAccessCondition.pp_description fmt c | BinaryOperation c -> BinaryOperationCondition.pp_description fmt c @@ -554,16 +561,16 @@ module Condition = struct let check = function | AllocSize c -> AllocSizeCondition.check c - | ArrayAccess {is_collection_add; c} -> - ArrayAccessCondition.check ~is_collection_add c + | ArrayAccess c -> + ArrayAccessCondition.check c | BinaryOperation c -> BinaryOperationCondition.check c let forget_locs locs x = match x with - | ArrayAccess {is_collection_add; c} -> - ArrayAccess {is_collection_add; c= ArrayAccessCondition.forget_locs locs c} + | ArrayAccess c -> + ArrayAccess (ArrayAccessCondition.forget_locs locs c) | AllocSize _ | BinaryOperation _ -> x end @@ -806,8 +813,9 @@ module ConditionSet = struct 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 + ArrayAccessCondition.make ~offset ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp + ~relation + |> Condition.make_array_access |> add_opt location val_traces condset diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 738b246f3..53a5b9a50 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -129,27 +129,27 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, zero_to_infty, 3, INTEGER_OVERFLOW_ codetoanalyze/c/bufferoverrun/minmax.c, exact_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/minmax.c, exact_min_plus_min_plus_min_UNDERRUN, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: x,Call,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [-19+min(0, x), -1] Size: 1] codetoanalyze/c/bufferoverrun/minmax.c, underapprox_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/models.c, call_memcpy_len2_Good_FP, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Offset: [0, +oo] Size: [0, +oo] by call to `memcpy_len` ] +codetoanalyze/c/bufferoverrun/models.c, call_memcpy_len2_Good_FP, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Offset added: [0, +oo] Size: [0, +oo] by call to `memcpy_len` ] codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, no_bucket, ERROR, [Here] codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 255] Size: 255] codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 256] Size: 256] codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1, 255] Size: 10000] -codetoanalyze/c/bufferoverrun/models.c, memcpy_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memcpy_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memcpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memcpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 8 Size: 4] -codetoanalyze/c/bufferoverrun/models.c, memmove_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memmove_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memmove_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memmove_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 8 Size: 4] -codetoanalyze/c/bufferoverrun/models.c, memset_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memset_bad2, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, memset_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 8 Size: 4] -codetoanalyze/c/bufferoverrun/models.c, strncpy_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, strncpy_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, strncpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 40] -codetoanalyze/c/bufferoverrun/models.c, strncpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 8 Size: 4] -codetoanalyze/c/bufferoverrun/models.c, strncpy_good5_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5] +codetoanalyze/c/bufferoverrun/models.c, memcpy_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memcpy_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memcpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: -1 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memcpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 8 Size: 4] +codetoanalyze/c/bufferoverrun/models.c, memmove_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memmove_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memmove_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: -1 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memmove_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 8 Size: 4] +codetoanalyze/c/bufferoverrun/models.c, memset_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memset_bad2, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: -1 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memset_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset added: 8 Size: 4] +codetoanalyze/c/bufferoverrun/models.c, strncpy_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, strncpy_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, strncpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: -1 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, strncpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 8 Size: 4] +codetoanalyze/c/bufferoverrun/models.c, strncpy_good5_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset added: 10 Size: 5] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop3_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop4_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 591110358..06bf1158b 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -8,14 +8,14 @@ codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):bool codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 884, degree = 0] codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 883, degree = 0] codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 890, degree = 0] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add3_overrun_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 4 Size: 3] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_addAll_bad():void, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 5 Size: 4] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add3_overrun_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset added: 4 Size: 3] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_addAll_bad():void, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset added: 5 Size: 4] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_ok():void, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 202, degree = 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_ok():void, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, degree = 0] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_overrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 0] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: -1 Size: 0] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_overrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset added: 1 Size: 0] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset added: -1 Size: 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 2 Size: 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 0 Size: 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1]