diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index f4f00aa05..e459e35a7 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -537,6 +537,18 @@ module Bound = struct when SymLinear.is_zero se -> let d = Sign.eval_neg_if_minus sign Z.(c2 - c1) in mk_MinMax (c1, sign, minmax, d, s) + | MinMax (c1, Plus, Min, d1, s1), Linear (c2, s2) + | Linear (c2, s2), MinMax (c1, Plus, Min, d1, s1) + when SymLinear.is_one_symbol_of s1 s2 -> + let c = Z.min c1 c2 in + let d = Z.(c1 + d1) in + mk_MinMax (c, Plus, Min, Z.(d - c), s1) + | MinMax (c1, Minus, Max, d1, s1), Linear (c2, s2) + | Linear (c2, s2), MinMax (c1, Minus, Max, d1, s1) + when SymLinear.is_mone_symbol_of s1 s2 -> + let c = Z.min c1 c2 in + let d = Z.(c1 - d1) in + mk_MinMax (c, Minus, Max, Z.(c - d), s1) | MinMax (c1, (Minus as sign), (Max as minmax), d1, s1), MinMax (c2, Minus, Max, d2, s2) | MinMax (c1, (Plus as sign), (Min as minmax), d1, s1), MinMax (c2, Plus, Min, d2, s2) when Symb.Symbol.equal s1 s2 -> diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 8dd0346cb..10838db08 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -180,6 +180,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVE codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [,Parameter `*n`,Assignment,,Parameter `*n`,Array declaration,Array access: Offset: [*n, +oo] Size: *n] codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [,Parameter `*n`,Assignment,,Parameter `*n`,Array declaration,Array access: Offset: [*n, +oo] Size: *n] codetoanalyze/c/bufferoverrun/issue_kinds.c, zero_to_infty, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] +codetoanalyze/c/bufferoverrun/minmax.c, call_exact_minmax_sym_Bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,Call,Parameter `x`,Assignment,,Assignment,Array declaration,Array access: Offset: [2, 5] Size: 5] 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, [,Parameter `x`,Call,Assignment,Assignment,Assignment,Assignment,,Array declaration,Array access: 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] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/minmax.c b/infer/tests/codetoanalyze/c/bufferoverrun/minmax.c index b2bc296b8..5c9cca569 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/minmax.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/minmax.c @@ -38,3 +38,27 @@ void exact_min_plus_min_plus_min_UNDERRUN(int x, int b) { // [-19 + min(0, x), -1] size1[y] = 0; } + +int random(); + +int exact_minmax_sym(int x) { + if (random()) { + if (x > 1) { + x = 1; + } // [min(1, x), 1] + x = x + 1; // [1 + min(1, x), 2] + } // [min(2, x), max(2, x)] + return x; +} + +void call_exact_minmax_sym_Good() { + int x = 5; + int a[x]; + a[exact_minmax_sym(x) - 1] = 0; +} + +void call_exact_minmax_sym_Bad() { + int x = 5; + int a[x]; + a[exact_minmax_sym(x)] = 0; +}