From 5c3acff09f9be19ee56099abd0aec50abaf042f4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 Feb 2022 23:53:02 +0000 Subject: [PATCH] goto_rw: byte extracts may have a negative offset A negative offset can be safely ignored as there is nothing to be read from or to be written to. Fixes: #2524 --- regression/cbmc/full_slice3/test.desc | 2 +- src/analyses/goto_rw.cpp | 5 +++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/regression/cbmc/full_slice3/test.desc b/regression/cbmc/full_slice3/test.desc index e226d5314a3..9f1003d166a 100644 --- a/regression/cbmc/full_slice3/test.desc +++ b/regression/cbmc/full_slice3/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --full-slice ^EXIT=0$ diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 7912995025f..458ff3106e0 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -163,8 +163,9 @@ void rw_range_sett::get_objects_byte_extract( be.op().type(), be.id()==ID_byte_extract_little_endian, ns); - range_spect offset = - range_start + map.map_bit(numeric_cast_v(*index)); + range_spect offset = range_start; + if(*index > 0) + offset += map.map_bit(numeric_cast_v(*index)); get_objects_rec(mode, be.op(), offset, size); } }