From 542ce54dcf1338b36a485c748aa90f31ba121e1d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 11 Mar 2022 21:39:52 +0000 Subject: [PATCH] goto_rw: left shift may be larger than object size While such an expression might have undefined behaviour in some source languages, goto_rw should not assert that a goto program does not contain such an expression. --- .../leftshift_overflow-c99-full-slice.desc | 17 +++++++++++++++++ src/analyses/goto_rw.cpp | 3 +-- 2 files changed, 18 insertions(+), 2 deletions(-) create mode 100644 regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc diff --git a/regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc b/regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc new file mode 100644 index 00000000000..4059cdb1c85 --- /dev/null +++ b/regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc @@ -0,0 +1,17 @@ +CORE +leftshift_overflow.c +--signed-overflow-check --c99 --full-slice +^EXIT=10$ +^SIGNAL=0$ +^\[.*\] 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 14 arithmetic overflow on signed shl in .*: .* +^\[.*\] line 23 arithmetic overflow on signed shl in .*: .* diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 8fc830c919c..b5da8044e44 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -217,9 +217,8 @@ void rw_range_sett::get_objects_shift( if(sh_range_start>=0 && sh_range_start= 0) { - assert(src_size-dist_r>=0); range_spect sh_size=std::min(size, src_size-dist_r); get_objects_rec(mode, shift.op(), range_start, sh_size);