diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 98c181272..a14cbbaab 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -82,7 +82,7 @@ module AllocSizeCondition = struct | cmp_big -> let propagate = match (cmp_mone, cmp_big) with - | `NotComparable, _ | _, `NotComparable -> + | (`NotComparable | `LeftSubsumesRight), _ | _, (`NotComparable | `LeftSubsumesRight) -> true | _ -> false diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c index fe35645f6..44da37b52 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c @@ -5,6 +5,22 @@ * LICENSE file in the root directory of this source tree. */ +int zero_or_ten(int ten) { + if (ten) { + return 10; + } else { + return 0; + } +} + +int zero_to_infty() { + int r = 0; + for (int i = 0; i < zero_or_ten(0); i++) { + r++; + } + return r; +} + void l1_concrete_overrun_Bad() { int a[10]; a[10] = 0; @@ -29,14 +45,6 @@ void l1_symbolic_underrun_Bad(int i) { } } -int zero_or_ten(int ten) { - if (ten) { - return 10; - } else { - return 0; - } -} - void l2_concrete_overrun_Bad() { int a[10]; a[zero_or_ten(1)] = 0; @@ -157,6 +165,17 @@ void alloc_may_be_big_Good_FP() { malloc(zero_or_ten(1) * 100 * 1000 * 1000 + 1); } +/* + When the upper bound is infinity and the lower bound unknown, + we don't report but still propagate the error. +*/ +void alloc_may_be_big2_Silenced(int n) { malloc(n + zero_to_infty()); } + +// Now that we have a lower bound, we can report it +void call_to_alloc_may_be_big2_is_big_Bad() { + alloc_may_be_big2_Silenced(100 * 1000 * 1000); +} + void l1_unknown_function_Bad() { int a[5]; int idx = unknown_function() * 10; @@ -167,14 +186,6 @@ void l1_unknown_function_Bad() { } } -int zero_to_infty() { - int r = 0; - for (int i = 0; i < zero_or_ten(0); i++) { - r++; - } - return r; -} - /* Inferbo raises U5 alarm because - the pair of offset:[10,10] and size:[5,+oo] is belong to L3 - the offset value is from an unknown function diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 221cdf902..ca8f69886 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -34,6 +34,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Bad, 0, INFERBO_AL codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Good_FP, 1, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [1, 1000000001]] codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [-5, 5]] codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Good_FP, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [-5, 5]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Bad, 1, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Call,Parameter: n,Alloc: Length: [100000000, +oo] by call to `alloc_may_be_big2_Silenced` ] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [max(10, i.lb), i.ub] Size: 10]