Byte update with a symbolic size does not write the partially covered last array element (unsound)

[bardiharborow]

CBMC version: 6.11.0 (cbmc-6.11.0)
Operating system: macOS 26.3, arm64
Exact command line resulting in the issue: cbmc main.c
What behaviour did you expect: both assertions pass
What happened instead: both assertions fail

#include <stdint.h>
#include <string.h>

int main()
{
  unsigned n;
  __CPROVER_assume(n == 5 || n == 6);
  unsigned char src[6] = {0xAA, 0xBB, 0xCC, 0xDD, 0xEE, 0xFF};
  uint32_t dst[2] = {0, 0};
  memcpy(dst, src, n);
  unsigned char *b = (unsigned char *)dst;
  __CPROVER_assert(b[4] == 0xEE, "byte 4 copied");
  __CPROVER_assert(n != 6 || b[5] == 0xFF, "byte 5 copied");
}

[main.assertion.1] line 15 byte 4 copied: FAILURE
[main.assertion.2] line 16 byte 5 copied: FAILURE
VERIFICATION FAILED

The copy fills dst[0] and writes one or two bytes into dst[1]. CBMC finds a trace in which dst[1] keeps its old value. The result is unsound.

Which cases are affected

The copy size must be symbolic, the destination must be an array of multi-byte elements, and the copy must end inside an element other than the first one. memcpy, memmove, memset and __CPROVER_array_replace are all affected. char arrays are not affected because they take a different lowering.

Cause

Symex produces a byte_update whose value has a non-constant size. The lowering goes to lower_byte_update_array_vector_unbounded. For the last, partially covered element it builds (L1752)

byte_update(dst[last_index], -(last_index * subtype_size), value)

where value is the whole update value of non-constant size, and lowers that. Two things go wrong:

1. The negative offset is meant to slide the value backwards so that its bytes last_index * subtype_size ... land on the element. The bit-vector path of lower_byte_update cannot do that for a value of non-constant size: it instantiates only the first sizeof(element) bytes of the value (L2425) and then shifts both the value and the mask right by the negated offset (L2535). With last_index == 1 the shift is by 32 bits, so the mask and the value are both zero and the element does not change.
2. The offset also ignores the offset of the update inside the first element. The correct offset relative to the element is src.offset() - last_index * subtype_size.

The element must instead receive the bytes of the update value starting at initial_bytes + subtype_size * (last_index - first_index - 1), of which only the remaining bound - that offset many are to be written. One way is to byte-extract subtype_size bytes at that position into a fixed-size byte array and apply a byte update at offset 0 whose update bound is the number of remaining bytes.