Skip to content

Commit 1e5b7aa

Browse files
authored
Merge pull request #2822 from diffblue/rw_range_lower_bound_fix
need to check lower bound on index in rw_range_sett::get_objects_byte_extract
2 parents 59ff926 + afac4a0 commit 1e5b7aa

File tree

2 files changed

+10
-3
lines changed

2 files changed

+10
-3
lines changed

regression/cbmc/full_slice3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--full-slice
44
^EXIT=0$

src/analyses/goto_rw.cpp

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -163,8 +163,15 @@ void rw_range_sett::get_objects_byte_extract(
163163
be.op().type(),
164164
be.id()==ID_byte_extract_little_endian,
165165
ns);
166-
range_spect offset =
167-
range_start + map.map_bit(numeric_cast_v<std::size_t>(*index));
166+
range_spect offset = range_start;
167+
if(*index > 0)
168+
offset += map.map_bit(numeric_cast_v<std::size_t>(*index));
169+
else
170+
{
171+
// outside the bounds of immediate byte-extract operand, might still be in
172+
// bounds of a parent object
173+
offset += to_range_spect(*index);
174+
}
168175
get_objects_rec(mode, be.op(), offset, size);
169176
}
170177
}

0 commit comments

Comments
 (0)