diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 7402ed01a..116dfb386 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -257,8 +257,10 @@ module ItvPure = struct of_big_int Z.(n mod m) | None -> let abs_m = Z.abs m in - if is_ge_zero x then (Bound.zero, Bound.of_big_int Z.(abs_m - one)) - else if is_le_zero x then (Bound.of_big_int Z.(one - abs_m), Bound.zero) + if is_ge_zero x then + (Bound.zero, Bound.overapprox_min (Bound.of_big_int Z.(abs_m - one)) (ub x)) + else if is_le_zero x then + (Bound.overapprox_max (Bound.of_big_int Z.(one - abs_m)) (lb x), Bound.zero) else (Bound.of_big_int Z.(one - abs_m), Bound.of_big_int Z.(abs_m - one)) ) diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/arith.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/arith.cpp index a7444c182..b7336b1f7 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/arith.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/arith.cpp @@ -5,6 +5,7 @@ * LICENSE file in the root directory of this source tree. */ #include +#include void sizeof_bool_Good() { int a[2]; @@ -115,3 +116,19 @@ void call_integer_overflow_param_1_Good() { integer_overflow_param_1(0); } uint32_t integer_overflow_param_2(uint32_t x) { return x - 1; } void call_integer_overflow_param_2_Bad() { integer_overflow_param_2(0); } + +void mod_ub(const char* msg, size_t leng) { + size_t rem = leng % 32; + if (rem == 15) { + char d = msg[14]; // Good + } + if (rem == 10) { + char d = msg[14]; // Bad + } +} + +void call_mod_ub_1_Good() { mod_ub("ab", 2); } + +void call_mod_ub_2_Good() { mod_ub("abcdefghijklmno", 15); } + +void call_mod_ub_Bad() { mod_ub("abcdefghij", 10); } diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 02e4616fc..339ec009b 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -9,6 +9,7 @@ codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Good_FP, 2, CONDITION_A codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/arith.cpp, call_integer_overflow_param_2_Bad, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `x`,Binary operation: (0 - 1):unsigned32 by call to `integer_overflow_param_2` ] codetoanalyze/cpp/bufferoverrun/arith.cpp, call_integer_overflow_x_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter `init`,Assignment,Call,,Parameter `this->x`,,Assignment,Binary operation: (4294967295 × 4294967295):unsigned32 by call to `RG::integer_overflow_x` ] +codetoanalyze/cpp/bufferoverrun/arith.cpp, call_mod_ub_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `*msg`,Array access: Offset: 14 Size: 11 by call to `mod_ub` ] codetoanalyze/cpp/bufferoverrun/arith.cpp, integer_overflow_field_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,Binary operation: (0 - 1):unsigned32] codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 2 Size: 2]