Fix unbounded recursion in byte-update lowering of structs

The missing update of the type of the byte-update expression caused the
very same procedure to be invoked recursively. Instead we should use
byte-update-of-array.

regression/cbmc/byte_update11/main.c

@@ -0,0 +1,13 @@
+struct S
+{
+  int i;
+};
+
+int main()
+{
+  unsigned x;
+  __CPROVER_assume(x % sizeof(int) == 0);
+  struct S A[x];
+  ((char *)A)[x] = 42;
+  __CPROVER_assert((A[x / sizeof(int)].i & 0xFF) == 42, "lowest byte is 42");
+}

regression/cbmc/byte_update11/test.desc

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

src/solvers/lowering/byte_operators.cpp

@@ -1787,6 +1787,10 @@ 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
+      // into a byte array, which we know how to update even if the offset is
+      // non-constant.
       const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
                                         ? ID_byte_extract_little_endian
                                         : ID_byte_extract_big_endian;
@@ -1802,6 +1806,7 @@ static exprt lower_byte_update_struct(
 
       byte_update_exprt bu = src;
       bu.set_op(lower_byte_extract(byte_extract_expr, ns));
+      bu.type() = bu.op().type();
 
       return lower_byte_extract(
         byte_extract_exprt{