[SwayamInSync]

Through a pointer, the verifier reached only a record's direct fields (p->x, (*p).x). Every deeper place was an error:

Access	0.1.1 and main
p->inner.y, p[k].x	unsupported aggregate field base expression
r->buf[i], p->inner.arr[j]	array-to-pointer decay of automatic storage is unsupported until lexical lifetime and escape effects are modeled

So a ring buffer, a fixed-capacity stack, or any record that keeps its storage inline could not be verified at all. The second message was also wrong about the cause: r->buf is not automatic storage.

Now each field and each fixed-array element of the object a pointer addresses is one heap cell, at any depth: p->f, p->inner.arr[j], p->grid[i][j], (*p).items[k].v, and p[k].buf[i] for an element of a valid(p, n) extent. Code can read and write it, contracts and cppverify::modifies footprints can name it (cells and ranges such as p->buf[0 : 8]), a reference can bind to it, it can be passed to a reference parameter, and a spec can read it.

struct Ring { int buf[8]; int head; int count; };

void put(Ring *r, int v)
  cppverify::pre(r != nullptr && 0 <= r->head && r->head < 8)
  cppverify::modifies(r->buf[r->head])
  cppverify::post(r->buf[r->head] == v && r->count == cppverify::old(r->count))
{
  r->buf[r->head] = v;
}

Design

Each access is checked twice:

• Against its own array. Every fixed-array index must lie in its array (0 <= i < 8, kind bounds), as Frama-C's RTE plugin generates index_bound and as Verus requires i < N for a [T; N] index.
• Against the object. The address must lie in the pointer's object (its valid(p, n) extent, or one object), as before, which corresponds to Frama-C's \valid.

Checking only one of them would miss errors. An object check alone (CompCert-style block validity) accepts r->buf[8], because its address is r->head, inside *r; it also accepts grid[0][4], which is grid[1][0] in memory. An index check alone says nothing about p itself.

In the converter, the place builder for promoted locals becomes objectPlace, which takes either root:

• Promoted local: its allocation, as before.
• The object a pointer addresses: a new pointeeRootPointer walks the selection chain down to p->, (*p)., or p[k]., and pointeePlace uses that pointer as the base.

Loads, stores, reference bindings (lvaluePlace), and reference arguments all go through objectPlace. The new place carries the access condition that local arrays already had, so passivization, UB instrumentation, and every backend are unchanged.

Two forms are rejected, with messages that name what is unsupported:

Form	Message
A whole record or array read through a pointer (Ring copy = *r;)	a record or array read as a whole through a pointer is unsupported; read its fields
A pointer to an array member (const int *q = r->buf;)	a pointer to the array member 'buf' is unsupported; index the member where it is used, as in 'buf[i]'

Such a pointer would have to carry the member's extent, the way a Rust slice carries its length. That is the next 0.2 item: a decayed member array gets an origin whose object is the member, so the pointer's accesses are bounded by the array. A decayed global array or global record member is also named now (the global array 'table' is unsupported, the array member 'buf' of the global 'g' is unsupported), instead of the automatic-storage message.

Tests

suite/pointer_subobjects.cpp, three runs:

• Proofs: reads and writes at every depth, modifies cells and ranges, a loop that clears a member array with a quantified invariant, a caller framed by that loop's function, a reference to an element, an element passed to int &, an element of a valid(p, n) extent, and a spec that reads elements.
• Failures, each with the expected counterexample:
  • one past the array, read, written, bound to a reference, passed by reference, and read in a postcondition: i = 8;
  • below zero: i = -1;
  • a row overflow in a 2D member: j = 4;
  • a write that may hit the cell a postcondition reads: i = j;
  • a write outside the frame;
  • a wrong postcondition after a nested write.
• Layer 1 dump: peek's load is r + 0 + cast(load(r + 32)) * 4 with the access condition 0 <= head < 8.
• Messages: the decay messages for a member through a pointer, a global record member, and a global array.

dynamic_loaded_values.cpp now expects the message that names the global array.

Docs

• structs.rst: a new "Records through pointers" section, with a checked example and its verdicts, and the two rejected forms.
• ch14: a fixed-capacity stack, with a checked example and verdicts. It explains the push_full counterexample, a store that would land on size.
• pointers.rst: the footprint cells and ranges.
• limitations.rst: the References, Arrays, and Records rows, and the supported-subset list.
• Release notes: an entry under "C++ that compiles now".
• DESIGN.md and ARCHITECTURE.md: the design above, and places inside objects.

Checked

On main at 5165654, with #45 and #47:

• Verify lit suite: 427 passed and 1 unsupported, on both the release build and an assertions build. This includes the docs tests (docs_examples.test, docs_coverage.test).
• VerifyTests: 60 passed, 1 skipped.
• On main: every RUN line of pointer_subobjects.cpp fails, as does the updated check in dynamic_loaded_values.cpp. main rejects each function in the file with the automatic-storage message.
• Verdict differential against main: 435 test sources, every function's status, reason, and qualifiers. Only pointer_subobjects.cpp differs, and no file's time changed (3531 s → 3506 s in total).
• Mutation: 12 mutants, all killed by the tests. They:
  • drop the pointer root from subscript places, field loads, stores, and reference bindings;
  • drop the index bound for pointer-rooted elements, or make it one too large;
  • drop a pointee store's access condition;
  • drop the *p root, or the p[k]. root inside a selection;
  • ignore an arrow member's offset;
  • make the decay messages generic.

Rebased on #45 and #47

• The new errors are reported through verify: Report each conversion error at its source, with its line and caret #47's error(...), so they carry their location and caret, like every other conversion error.
• The decay checks in the test now check the location too (pointer_subobjects.cpp:N:18: error: decayed: ...).
• The rejected example in structs.rst passes r->buf to a buffer parameter and shows the located error. The earlier example (const int *q = r->buf; return q[0];) also printed a second error, about reading q, that follows from the first; E2b removes such follow-on errors.
• The limitations.rst References row keeps docs: Correct the public documentation the 0.2 audit found wrong #45's text and adds the fields and elements of a record a pointer addresses.