Byte-extract lowering: do not blindly use offsets

When unpacking an array we must not create 0 bytes up until an offset
when the source array can never be as large. Doing so when within a
struct would spuriously produce a larger member.

Fixes: #7654

Author: tautschnig

regression/cbmc/byte_extract2/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+#define SIZE 1
+
+struct s
+{
+  char a1[1];
+  unsigned int a2_len;
+  char a2[SIZE];
+};
+
+void main()
+{
+  struct s s1;
+  char buf[SIZE];
+
+  __CPROVER_assume(s1.a2_len <= SIZE);
+  __CPROVER_assume(s1.a2_len >= SIZE);
+  char src_n[s1.a2_len];
+  __CPROVER_array_copy(src_n, s1.a2);
+  assert(src_n[0] == s1.a2[0]);
+}

regression/cbmc/byte_extract2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/util/lower_byte_operators.cpp

@@ -777,14 +777,10 @@ static array_exprt unpack_struct(
       !bit_fields.has_value(),
       "all preceding members should have been processed");
 
-    exprt sub = unpack_rec(
-      member,
-      little_endian,
-      offset_in_member,
-      max_bytes_left,
-      bits_per_byte,
-      ns,
-      true);
+    // TODO: we could do better, perhaps checking whether this component needs
+    // to be unpacked at all
+    exprt sub =
+      unpack_rec(member, little_endian, {}, {}, bits_per_byte, ns, true);
 
     byte_operands.insert(
       byte_operands.end(),