diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index a6e024c5e..7fb3448e1 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -227,14 +227,32 @@ module ItvPure = struct | Some n -> if NonZeroInt.is_one n then itv else if NonZeroInt.is_minus_one n then neg itv - else if NonZeroInt.is_positive n then - let l' = Option.value ~default:Bound.minf (Bound.div_const_l l n) in - let u' = Option.value ~default:Bound.pinf (Bound.div_const_u u n) in - (l', u') else - let l' = Option.value ~default:Bound.minf (Bound.div_const_l u n) in - let u' = Option.value ~default:Bound.pinf (Bound.div_const_u l n) in - (l', u') + let l', u' = + if NonZeroInt.is_positive n then (Bound.div_const_l l n, Bound.div_const_u u n) + else (Bound.div_const_l u n, Bound.div_const_u l n) + in + let default_l, default_u = + if Bound.(le zero l) then + if NonZeroInt.is_positive n then + (* if 0<=l<=u and 0 t -> t = diff --git a/infer/tests/codetoanalyze/c/performance/cost_test.c b/infer/tests/codetoanalyze/c/performance/cost_test.c index 7f607a2be..c8c16ca97 100644 --- a/infer/tests/codetoanalyze/c/performance/cost_test.c +++ b/infer/tests/codetoanalyze/c/performance/cost_test.c @@ -158,3 +158,11 @@ void ignore_character_symbols_constant_FP(char c) { } } } + +unsigned int div_const(unsigned int n) { return n / 2; } + +void iter_div_const_constant() { + unsigned int n = div_const(20); + for (int i = 0; i < n; i++) { + } +}