Limit dereferencing of __CPROVER_bitvector to objects with size multiple of 8

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;
+}

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

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