diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index ba1266f3f..ed1af90db 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -263,15 +263,17 @@ module ItvPure = struct (* x >> [-1,-1] does nothing. *) let shiftrt : t -> t -> t = fun x y -> - match is_const y with - | Some n when Z.(leq n zero) -> - x - | Some n when Z.(n >= of_int 64) -> - zero - | Some n -> ( - match Z.to_int n with n -> div_const x Z.(one lsl n) | exception Z.Overflow -> top ) - | None -> - top + if is_zero x then x + else + match is_const y with + | Some n when Z.(leq n zero) -> + x + | Some n when Z.(n >= of_int 64) -> + zero + | Some n -> ( + match Z.to_int n with n -> div_const x Z.(one lsl n) | exception Z.Overflow -> top ) + | None -> + top let band_sem : t -> t -> t = diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index 2d3f66864..d26588456 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -530,3 +530,15 @@ int check_addition_overflow_Good(unsigned int x, unsigned int y) { return 0; } } + +void shift_right_zero_Good(int x) { + int arr[1]; + arr[0 >> x] = 1; +} + +/* This also exhibits an overapproximation of traces, here [x] doesn't influence + * the result */ +void shift_right_zero_Bad(int x) { + int arr[1]; + arr[1 + (0 >> x)] = 1; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 5256a6efc..a69030e24 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -35,6 +35,7 @@ codetoanalyze/c/bufferoverrun/arith.c, recover_integer_underflow_Bad, 3, INTEGER codetoanalyze/c/bufferoverrun/arith.c, recover_integer_underflow_Good_FP, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [,Assignment,Binary operation: ([0, 9] - 1):unsigned32] codetoanalyze/c/bufferoverrun/arith.c, scan_hex_Good, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/arith.c, scan_hex_Good, 8, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/arith.c, shift_right_zero_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `x`,,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/arith.c, simple_overflow_Bad, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Binary operation: (85 × 4294967295):unsigned32] codetoanalyze/c/bufferoverrun/arith.c, two_safety_conditions2_Bad, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Call,Assignment,Assignment,,Assignment,Binary operation: ([0, +oo] + [0, 80]):unsigned32] codetoanalyze/c/bufferoverrun/arith.c, unused_integer_underflow2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,Binary operation: (0 - 1):unsigned32]