From ba34966eb5f8435760473a9df560d3eb0d3ac25b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 7 Jan 2019 16:56:58 +0000 Subject: [PATCH] test signed left-shift overflow for C99 The semantics of signed left shifts are contentious for the case that a '1' is shifted into the signed bit. This tests the C99 case. --- .../cbmc/Overflow_Leftshift1/test-c99.desc | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 regression/cbmc/Overflow_Leftshift1/test-c99.desc diff --git a/regression/cbmc/Overflow_Leftshift1/test-c99.desc b/regression/cbmc/Overflow_Leftshift1/test-c99.desc new file mode 100644 index 00000000000..b12750a9c83 --- /dev/null +++ b/regression/cbmc/Overflow_Leftshift1/test-c99.desc @@ -0,0 +1,16 @@ +CORE +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 +^VERIFICATION FAILED$ +-- +^warning: ignoring +^\[.*\] line 12 arithmetic overflow on signed shl in .*: .* +^\[.*\] line 21 arithmetic overflow on signed shl in .*: .*