diff --git a/regression/cbmc/Overflow_Leftshift1/main.c b/regression/cbmc/Overflow_Leftshift1/main.c index 7d52799f096..2f1210ac5af 100644 --- a/regression/cbmc/Overflow_Leftshift1/main.c +++ b/regression/cbmc/Overflow_Leftshift1/main.c @@ -1,3 +1,5 @@ +#include + int main() { unsigned char x; @@ -23,5 +25,9 @@ int main() // not an overflow in ANSI-C, but undefined in C99 s = 1 << (sizeof(int) * 8 - 1); + // overflow in an expression where operand and distance types are different + uint32_t u32; + int64_t i64 = ((int64_t)u32) << 32; + return 0; } diff --git a/regression/cbmc/Overflow_Leftshift1/test-c89.desc b/regression/cbmc/Overflow_Leftshift1/test-c89.desc index 88d83ff7a86..d404408aeca 100644 --- a/regression/cbmc/Overflow_Leftshift1/test-c89.desc +++ b/regression/cbmc/Overflow_Leftshift1/test-c89.desc @@ -3,14 +3,15 @@ main.c --signed-overflow-check --c89 ^EXIT=10$ ^SIGNAL=0$ -^\[.*\] line 6 arithmetic overflow on signed shl in .*: FAILURE$ -^\[.*\] line 9 arithmetic overflow on signed shl in .*: SUCCESS$ -^\[.*\] line 15 arithmetic overflow on signed shl in .*: SUCCESS$ -^\[.*\] line 18 arithmetic overflow on signed shl in .*: FAILURE$ -^\*\* 2 of 5 failed +^\[.*\] line 8 arithmetic overflow on signed shl in .*: FAILURE$ +^\[.*\] line 11 arithmetic overflow on signed shl in .*: SUCCESS$ +^\[.*\] line 17 arithmetic overflow on signed shl in .*: SUCCESS$ +^\[.*\] line 20 arithmetic overflow on signed shl in .*: FAILURE$ +^\[.*\] line 30 arithmetic overflow on signed shl in .*: SUCCESS$ +^\*\* 2 of 6 failed ^VERIFICATION FAILED$ -- ^warning: ignoring -^\[.*\] line 12 arithmetic overflow on signed shl in .*: .* -^\[.*\] line 21 arithmetic overflow on signed shl in .*: .* -^\[.*\] line 24 arithmetic overflow on signed shl in .*: .* +^\[.*\] line 14 arithmetic overflow on signed shl in .*: .* +^\[.*\] line 23 arithmetic overflow on signed shl in .*: .* +^\[.*\] line 26 arithmetic overflow on signed shl in .*: .* diff --git a/regression/cbmc/Overflow_Leftshift1/test-c99.desc b/regression/cbmc/Overflow_Leftshift1/test-c99.desc index b12750a9c83..4e4ea5f9070 100644 --- a/regression/cbmc/Overflow_Leftshift1/test-c99.desc +++ b/regression/cbmc/Overflow_Leftshift1/test-c99.desc @@ -3,14 +3,15 @@ main.c --signed-overflow-check --c99 ^EXIT=10$ ^SIGNAL=0$ -^\[.*\] line 6 arithmetic overflow on signed shl in .*: FAILURE$ -^\[.*\] line 9 arithmetic overflow on signed shl in .*: SUCCESS$ -^\[.*\] line 15 arithmetic overflow on signed shl in .*: SUCCESS$ -^\[.*\] line 18 arithmetic overflow on signed shl in .*: FAILURE$ -^\[.*\] line 24 arithmetic overflow on signed shl in .*: FAILURE$ -^\*\* 3 of 6 failed +^\[.*\] line 8 arithmetic overflow on signed shl in .*: FAILURE$ +^\[.*\] line 11 arithmetic overflow on signed shl in .*: SUCCESS$ +^\[.*\] line 17 arithmetic overflow on signed shl in .*: SUCCESS$ +^\[.*\] line 20 arithmetic overflow on signed shl in .*: FAILURE$ +^\[.*\] line 26 arithmetic overflow on signed shl in .*: FAILURE$ +^\[.*\] line 30 arithmetic overflow on signed shl in .*: FAILURE$ +^\*\* 4 of 7 failed ^VERIFICATION FAILED$ -- ^warning: ignoring -^\[.*\] line 12 arithmetic overflow on signed shl in .*: .* -^\[.*\] line 21 arithmetic overflow on signed shl in .*: .* +^\[.*\] line 14 arithmetic overflow on signed shl in .*: .* +^\[.*\] line 23 arithmetic overflow on signed shl in .*: .* diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index f2d3043e433..d1254979b1f 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -777,8 +777,10 @@ void goto_checkt::integer_overflow_check( if(distance_type.id() == ID_unsignedbv) neg_dist_shift = false_exprt(); else - neg_dist_shift = - binary_relation_exprt(op, ID_lt, from_integer(0, distance_type)); + { + neg_dist_shift = binary_relation_exprt( + distance, ID_lt, from_integer(0, distance_type)); + } // shifting a non-zero value by more than its width is undefined; // yet this isn't an overflow