From 3cca95cf26fc3e7bbddfb70d7709035f1a1ec5b5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 9 Mar 2022 17:21:08 +0000 Subject: [PATCH] goto_rw: do not assume that all types have constant size pointer_offset_bits returns nullopt whenever the size of a type is not a numeric constant. Such cases arise when arrays have runtime-determined size, as is the case in regression test byte_update5. All other places except the one fixed in this commit already considered the case that pointer_offset_bits returns nullopt. --- regression/cbmc/byte_update5/full-slice.desc | 8 ++++++++ src/analyses/goto_rw.cpp | 9 +++++++-- 2 files changed, 15 insertions(+), 2 deletions(-) create mode 100644 regression/cbmc/byte_update5/full-slice.desc 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(