[SwayamInSync]

A reference to a record was an error, so the free-function form of a method on an object could not be verified. On the base:

counter.cpp:6:6: error: bump: unsupported C++ type in verification: Counter &

Now a Counter & (or const Counter &), as a parameter or a local, is a pointer to its object that is never null and never reseated:

struct Counter { int n; int limit; };
struct Pair { Counter left; Counter right; };

void reset(Counter &c)
  cppverify::modifies(c)
  cppverify::post(c.n == 0 && c.limit == 10)
{
  c.n = 0;
  c.limit = 10;
}

void reset_left(Pair &p)
  cppverify::modifies(p.left)
  cppverify::post(p.left.n == 0 && p.right.n == cppverify::old(p.right.n))
{
  reset(p.left);
}

void reset_count(Pair &p)
  cppverify::modifies(p.left.n)
{
  reset(p.left);
}

Verified: reset [backend=z3]
Verified: reset_left [backend=z3]
pair.cpp:22:3: error: verification failed: reset_count [...::frame@22:3] (counterexample: p [ssa=p_0] [type=pointer] = 1; trace: call.reset@22:3 arg0=1) [backend=z3] [reason=counterexample]

Stacked on #69 (B3a-3 of extras plan item B3a; B3a-1 #50 and B3a-2 #53 are merged).

Design

• References. A reference is initialized to refer to a valid object and cannot be reseated ([dcl.ref]), so it is a pointer that is never null and never changes. Dafny's modifies c is every field of the object c references and modifies c`n one field. Here a reference to a record gets exactly what 3b gives a pointer to a record: c.f, c.buf[i], c.inner.x are cells, each access with its array-index check and its object check, and &c.f and c.buf are subobject pointers with bounds. cppverify::modifies(c) is the object, cppverify::modifies(c.n) one cell.
• A record by value is its fields; a reference is an address. getRecordFromType looked through references, a remnant of a design that would have flattened C& into param.field values. It now stops at them, so source variables (c [ssa=c_0] in counterexamples), type-invariant injection, parameter lists, and call arguments treat a reference as the address it is. A record's type invariant is not injected for a reference, as for a pointer.
• Places. recordReferenceRoot finds the reference parameter or local a selection chain starts at, and inPointeeObject (it, or pointeeRootPointer) replaces pointeeRootPointer wherever a place through a pointer is admitted: loads, stores, subscripts, reference bindings, footprints, pointer-difference operands. objectPlace of a bare reference is the place at its address, as *p.
• Frames. VFunction::ReferenceParams decided that every reference's modifies(r) is one cell, which is right for a scalar reference (it may bind a field of a larger object) and wrong for a record, whose cell then had no logic sort (obligation lowering failed: frame (invalid sort in obligation IR) at a call). The set is now ScalarReferenceParams; a record reference's footprint is a region, its entry object, as *p.
• Members named whole. cppverify::modifies(p->left), for a member that is a record or array, was one cell holding the whole member, through a pointer as well: no store lies in it, so a function writing p->left.n failed frame, and so did reset(&p->left). convertFootprint now lowers a record or array named whole inside an object (p->inner, c.buf, p[k] of a record extent) to a range of one element of its size, so every frame path (own stores, call havoc, containment, loop frames) treats it as its bytes. *p and a bare reference stay regions.
• Local references bind a place as a parameter does (Counter &r = p->left;, = a[i], = other_ref, chained, inside loops) and may bind a promoted local record, whose reads and writes keep their lifetime and initialization checks through the reference's provenance companion. A pointer formed through such a reference (&r.n, r.buf) would not carry the local's lifetime, so subobjectPointerRoot admits pointer formation only through a pointer or a reference whose object outlives the function (a parameter, or a local not bound to represented storage), and the existing &local and decay errors apply otherwise.

What stays out (fail-closed)

• A local record passed to a reference or pointer parameter: the non-escape scan that admits a local scalar actual does not cover records, so the call stays Unresolved [construct.unsupported]; the message now says "the address of local or dynamic storage is passed to bump" (it said "a pointer to", wrong for a reference). This is B3a-4, next.
• A callee whose footprint is a whole record lies in the caller's frame only if one caller footprint contains it: the heap has a cell at every address, so modifies(p.left.n, p.left.limit) does not contain reset(p.left)'s footprint. Documented and tested.
• Whole-record reads through a reference, reference returns, rvalue and volatile references, references in spec and proof functions.

Tests

suite/record_references.cpp: Z3, BMC, and a VCR dump.

• reads, writes, const references, &c of a whole reference passed to a pointer callee, references passed on from a reference, *p, p.left; two mutable references disjoint (frame(c, c) fails aliasing), aliases honored (may_alias fails its postcondition with distinct objects), two const references may alias;
• modifies(c) verified, a store outside modifies(c.n) fails frame, a callee's whole object outside the caller's cell fails frame (reference and member), the fields-one-by-one case;
• members named whole, through a reference (left_only) and a pointer (right_only), and their VCR (range 8 / 1);
• array members: r.buf[r.head], an index past the array fails bounds, a decayed member passed to a buffer callee, &r.head and one past it (bounds);
• local references to *p, p->left, chained, a[i] in a loop, one past an extent (dereference), a local record (verified and an uninitialized field read failing initialization);
• the type invariant applies by value and not by reference;
• rejected: a local record to a callee (construct.unsupported, with the message), &r.head and r.buf through a reference to a local, a whole-record read, a proof function's reference, rvalue and volatile references.

references_unsupported.cpp no longer expects Pair & to be rejected.

Mutants, each built and run on record_references.cpp and the 13 reference, subobject, and record-layout tests beside it: 12 of 12 killed, all by record_references.cpp. A thirteenth, accepting volatile Counter &, survived because the explicit volatile check was dead (the pointer type check already rejects a volatile pointee); that check, and an equally unreachable collection check (Sema keeps collections out of executable code, and spec and proof functions take no references), are removed.

Mutant	Killed by
record reference parameters rejected (the base)	record_references
every reference parameter a one-cell footprint (the base)	record_references
a member named whole is one cell (the base)	record_references
a pointer formed through a reference to a local	record_references
local record references are not place roots	record_references
local record references rejected	record_references
getRecordFromType sees through references (the base)	record_references
a bare record reference has no place	record_references
places through a reference are not object places	record_references
places through references are not in an object	record_references
a member footprint of one byte	record_references
a member footprint of no element	record_references

The member mutant on its own reproduces the base for pointers: left_only(Pair *p) under modifies(p->left) fails frame at reset(&p->left), and its caller ends Unresolved: obligation lowering failed: caller (invalid sort in obligation IR).

Docs

• structs.rst: "Records through references", a checked example (four verified, reset_count fails frame), what is not yet supported; type invariants not injected for references.
• ch14: references to records with the records through pointers, the member-named-whole footprint.
• limitations.rst, index.rst: references to records supported; what remains.
• Release notes: "Records through references" (C++ that compiles now) and "A record member named whole in cppverify::modifies" (failures that were not real).
• DESIGN.md: 3c, footprints, type invariants. ARCHITECTURE.md: records through references, footprints.

Checked

• The Verify suite on a release build: 452 passed (the exhaustive decoder filtered out), 1200 s with 40 workers.
• After the last change (the dead checks, formatting, one more test case): the 16 reference, subobject, record, and docs tests, docs_examples.test included, pass.
• record_references.cpp on the base: every function taking a Counter & is an error.
• The same record-reference cases on BMC, cvc5, --no-check-ub, --int-encoding=bitvector, and a Lean export give the same verdicts or export.