diff --git a/regression/cbmc/byte_update5/full-slice.desc b/regression/cbmc/byte_update5/full-slice.desc new file mode 100644 index 00000000000..35702fdf3a2 --- /dev/null +++ b/regression/cbmc/byte_update5/full-slice.desc @@ -0,0 +1,8 @@ +CORE +main.c +--little-endian --full-slice +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index f8b16f285e3..8fc830c919c 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -148,15 +148,20 @@ void rw_range_sett::get_objects_byte_extract( const range_spect &range_start, const range_spect &size) { + auto object_size_bits_opt = pointer_offset_bits(be.op().type(), ns); const exprt simp_offset=simplify_expr(be.offset(), ns); auto index = numeric_cast(simp_offset); - if(range_start == -1 || !index.has_value()) + if( + range_start == -1 || !index.has_value() || + !object_size_bits_opt.has_value()) + { get_objects_rec(mode, be.op(), -1, size); + } else { *index *= 8; - if(*index >= *pointer_offset_bits(be.op().type(), ns)) + if(*index >= *object_size_bits_opt) return; endianness_mapt map(