diff --git a/regression/ansi-c/Issue_7104_Bv_Size/deref.c b/regression/ansi-c/Issue_7104_Bv_Size/deref.c new file mode 100644 index 00000000000..03ed31cc694 --- /dev/null +++ b/regression/ansi-c/Issue_7104_Bv_Size/deref.c @@ -0,0 +1,18 @@ +struct Foo1 +{ + __CPROVER_bitvector[1] m_array[2]; +}; +struct Foo8 +{ + __CPROVER_bitvector[8] m_array[2]; +}; + +int main(void) +{ + struct Foo1 f1; + struct Foo8 f8; + + __CPROVER_assert(f1.m_array[1] == *(f1.m_array + 1), ""); + __CPROVER_assert(f8.m_array[1] == *(f8.m_array + 1), ""); + return 0; +} diff --git a/regression/ansi-c/Issue_7104_Bv_Size/deref.desc b/regression/ansi-c/Issue_7104_Bv_Size/deref.desc new file mode 100644 index 00000000000..40063c609da --- /dev/null +++ b/regression/ansi-c/Issue_7104_Bv_Size/deref.desc @@ -0,0 +1,13 @@ +CORE +deref.c + +^EXIT=1$ +^SIGNAL=0$ +only bitvectors of size multiple of 8 bits can be dereferenced +^CONVERSION ERROR$ +-- +-- +This is checking that dereferenced __CPROVER_bitvectors always have a size +that is a multiple of 8. + +For more information, please have a look at https://github.com/diffblue/cbmc/issues/7104 diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index 01cb688063f..c21f8bbaa27 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -40,6 +40,13 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) } const std::size_t width = boolbv_width(expr.type()); + if(width % 8 != 0) + { + // throw invalid_source_file_exceptiont{ + // "only bitvectors of size multiple of 8 bits can be dereferenced", + // expr.source_location()}; + conversion_failed(expr); + } // special treatment for bit-fields and big-endian: // we need byte granularity