diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 84dc7adc2..2162dde3b 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -558,7 +558,7 @@ module Bound = struct let overapprox_min original_b1 b2 = - let rec overapprox_min b1 b2 = + let overapprox_min b1 b2 = exact_min b1 b2 ~otherwise:(fun b1 b2 -> match (b1, b2) with | ( MinMax (c1, (Minus as sign1), (Max as minmax1), d1, s1) @@ -607,17 +607,9 @@ module Bound = struct let v = if Z.leq vmin vmeet && Z.leq vmeet vmax then vmeet else vmax in let d = Sign.eval_neg_if_minus sign1 Z.(v - c1) in mk_MinMax (c1, sign1, minmax1, d, s1) - | _ -> ( - match big_int_ub b2 with - | Some v2 when not (is_const b2) -> - overapprox_min b1 (Linear (v2, SymLinear.zero)) - | _ -> ( - match big_int_ub b1 with - | Some v1 when not (is_const b1) -> - overapprox_min (Linear (v1, SymLinear.zero)) b2 - | _ -> - (* When the result is not representable, our best effort is to return the first original argument. Any other deterministic heuristics would work too. *) - original_b1 ) ) ) + | _ -> + (* When the result is not representable, our best effort is to return the first original argument. Any other deterministic heuristics would work too. *) + original_b1 ) in overapprox_min original_b1 b2 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 1c30f205f..27bbb732b 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -260,7 +260,8 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALW codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Call,Assignment,Assignment,,Array declaration,Array access: Offset: [-28, 16] Size: 17] codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_sym_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Call,Assignment,Assignment,,Array declaration,Array access: Offset: [-28, 16] Size: 17] codetoanalyze/c/bufferoverrun/prune_constant.c, call_greater_than_Good_FP, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,Binary operation: (0 - 1):unsigned32] -codetoanalyze/c/bufferoverrun/prune_constant.c, call_null_pruning_symbols_Good_FP, 0, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,,Parameter `a`,Assignment,,Parameter `a`,Assignment,Array declaration,Array access: Offset: [0, 29] Size: [1, 30] by call to `null_pruning_symbols` ] +codetoanalyze/c/bufferoverrun/prune_constant.c, call_null_pruning_symbols_3_Good_FP, 7, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Assignment,Call,,Parameter `a`,Assignment,,Parameter `a`,Assignment,Array declaration,Array access: Offset: [-1, 9] Size: [0, 10] by call to `null_pruning_symbols` ] +codetoanalyze/c/bufferoverrun/prune_constant.c, call_null_pruning_symbols_3_Good_FP, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Assignment,Call,,Parameter `a`,Assignment,Binary operation: ([0, 10] - 1):unsigned32 by call to `null_pruning_symbols` ] codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_add2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_add2` ] codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_sub2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_sub2` ] codetoanalyze/c/bufferoverrun/prune_constant.c, null_pruning1_Bad, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c index b3317b123..057b4a662 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c @@ -182,4 +182,18 @@ void null_pruning_symbols(unsigned int a, unsigned int b) { } } -void call_null_pruning_symbols_Good_FP() { null_pruning_symbols(10, 20); } +void call_null_pruning_symbols_1_Good() { null_pruning_symbols(10, 20); } + +void call_null_pruning_symbols_2_Good() { null_pruning_symbols(0, 0); } + +int unknown_function(); + +void call_null_pruning_symbols_3_Good_FP() { + unsigned int c; + if (unknown_function()) { + c = 0; + } else { + c = 10; + } + null_pruning_symbols(c, 0); +}