diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 5091be08e..776e7d55b 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -750,8 +750,8 @@ module ItvPure = struct let prune_diff : t -> Bound.t -> t bottom_lifted = fun ((l, u) as itv) b -> - if Bound.eq l b then normalize (Bound.plus_l l Bound.one, u) - else if Bound.eq u b then normalize (l, Bound.plus_u u Bound.mone) + if Bound.le b l then normalize (prune_gt itv (of_bound b)) + else if Bound.le u b then normalize (prune_lt itv (of_bound b)) else NonBottom itv diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index 6079abe00..0b635b609 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -247,7 +247,7 @@ void unsigned_prune_zero1_Good(unsigned int x) { } } -void call_unsigned_prune_zero1_Good_FP() { unsigned_prune_zero1_Good(0); } +void call_unsigned_prune_zero1_Good() { unsigned_prune_zero1_Good(0); } void unsigned_prune_zero2_Good(unsigned int y) { unsigned int x = y; diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index cdcab09b5..50a811920 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -1,6 +1,5 @@ codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: s,Binop: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ] codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ] -codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_zero1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_zero1_Good` ] codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_zero2_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: y,Assignment,Binop: ([-oo, 0] - 1):unsigned32 by call to `unsigned_prune_zero2_Good` ] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (2000000000 + 2000000000):signed32] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []