Merge pull request #6723 from tautschnig/bugfixes/goto_rw-left-shift

goto_rw: left shift may be larger than object size

Author: tautschnig

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 .*: .*

src/analyses/goto_rw.cpp

@@ -217,9 +217,8 @@ void rw_range_sett::get_objects_shift(
       if(sh_range_start>=0 && sh_range_start<src_size)
         get_objects_rec(mode, shift.op(), sh_range_start, sh_size);
     }
-    else
+    if(src_size - dist_r >= 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);