Merge pull request #7360 from tautschnig/bugfixes/b-e-zero

Byte-extract lowering: extracting zero-width struct members is fine

Author: tautschnig

regression/cbmc-library/memcpy-09/main.c

@@ -0,0 +1,37 @@
+#include <assert.h>
+#include <string.h>
+
+union _5557197549936569444_union
+{
+};
+
+struct _5557197549936569444
+{
+  // _case
+  unsigned char _case;
+  // cases -- this member makes all the difference
+  union _5557197549936569444_union cases;
+};
+
+struct _3036371764910125196
+{
+  // t
+  struct _5557197549936569444 t;
+  // array
+  unsigned char array[8l];
+};
+
+void main(void)
+{
+  struct _3036371764910125196 data = {.t = {._case = 0}, .array = {0}};
+  unsigned long int index;
+  if(index < 2)
+  {
+    unsigned char array[4] = {0, 0, 0, 0};
+    unsigned long start = index * 4ul;
+    unsigned long end = start + 4ul;
+
+    memcpy((unsigned char *)&data.array + start, array, end - start);
+    assert(data.t._case == 0);
+  }
+}

regression/cbmc-library/memcpy-09/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+memcpy of objects with zero-width fields at a non-constant offset and with a
+non-constant copy width must not result in spurious verification failures.
+Example constructed from https://github.com/model-checking/kani/issues/1911.

src/util/lower_byte_operators.cpp

@@ -1286,7 +1286,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
 
       // the next member would be misaligned, abort
       if(
-        !component_bits.has_value() || *component_bits == 0 ||
+        !component_bits.has_value() ||
         *component_bits % src.get_bits_per_byte() != 0)
       {
         failed = true;
@@ -1992,7 +1992,7 @@ static exprt lower_byte_update_struct(
     else if(!offset_bytes.has_value())
     {
       // The offset to update is not constant; abort the attempt to update
-      // indiviual struct members and instead turn the operand-to-be-updated
+      // individual struct members and instead turn the operand-to-be-updated
       // into a byte array, which we know how to update even if the offset is
       // non-constant.
       auto src_size_opt = size_of_expr(src.type(), ns);