[SwayamInSync]

A function that requires valid(p, n) accepted an argument only when the argument was written as one of the caller's parameters plus an offset. Any other argument failed with a counterexample, even when the program was correct. That is a wrong Failed verdict, in 0.1.1 and on main:

int first(const int *p, int n)
  cppverify::pre(cppverify::valid(p, n) && n >= 1)
  cppverify::post(cppverify::result == p[0])
{
  return p[0];
}

int copied(const int *a)
  cppverify::pre(cppverify::valid(a, 4))
  cppverify::post(cppverify::result == a[1])
{
  const int *q = a + 1;
  return first(q, 3);   // main: verification failed [bounds] (counterexample: a = 1, q = 5)
}

first(a + 1, 3) verified, but first(q, 3) with q = a + 1 did not. The same happened for:

• a choice between pointers (c ? a + 1 : b);
• a pointer stepped in a loop (q = q + 1 with an invariant q == a + i);
• a callee's result whose contract says where it points (post(result == a + 1));
• an empty slice at one past the end (q = a + 4; count(q, 0)).

Cause

At a call, sliceContainment (Passivize.cpp) proves an extent argument's containment syntactically. The argument's base must be a caller parameter with an extent; otherwise the obligation is the literal false, of kind bounds. The callee's validity precondition ValidPtr(actual) was likewise discharged only by rewriting the actual to that parameter base. A literal false is refuted by any model, so the result was a "certified" counterexample about a correct program.

Fix

Containment is now semantic, as access checks already are:

• Containment: in the object model, an argument the syntactic rule cannot place is contained when its bytes [actual, actual + n * S] lie in one of the caller's objects. These are the entry objects its origins name (the objects it may address), or any of the caller's objects when its origins are unknown, as for a call result (Passivizer::objectContainment). Validity is a property of storage, so any object that contains the elements establishes it; origins only narrow the disjunction. This is the same rule a single-object argument already follows (abstractValidity).
• Validity precondition: for a precondition that mentions an extent parameter whose argument is not written from a caller parameter, ValidPtr(actual) is discharged by the same membership.

Where the syntactic rule applies, the call produces exactly the query it did before. Only calls whose containment was the literal false change. Both changes replace a check that could never succeed by one that holds exactly when the argument's elements lie in the caller's storage, so a false claim cannot verify. The test's false twins check this: three elements from a + 2, a choice whose a side is too short, a result whose contract does not place it, and a walk that stops too early.

This also prepares B3a-2. A pointer to an array member passed to a buffer function needs this containment, and B3a-2 adds the member's bounds to it.

Tests

suite/slice_argument_objects.cpp contains:

• Proofs: a copy (read and written), a choice, a callee result, an empty slice at one past the end, and a stepped pointer.
• Failures: each with its counterexample at the call, including c = true for the choice, and a trusted result one element before a, whose slice would end inside a.

On main every function in the file except the callees fails.

Docs

• pointers.rst: the modular-calls paragraph states the rule, with a checked example and its verdicts.
• Other pages: the same rule in limitations.rst, book chapters 14, 17, and 18, DESIGN.md, and ARCHITECTURE.md.
• Release notes: an entry under "Failures that were not real".

Checked

On main at 5165654:

• Verify lit suite: 427 passed and 1 unsupported, on both the release build and an assertions build. This includes the docs tests.

• VerifyTests: 60 passed, 1 skipped.

• On main: slice_argument_objects.cpp fails.

• Verdict differential against main: 435 test sources. Only the new test differs, and no file's time changed (3530 s → 3501 s in total). An earlier version added the object containment to every extent call, and in that version decode_uleb128_length_11 timed out. Using it only where the syntactic rule fails keeps every other query as it was.

• Mutation: 8 mutants, all killed by the test. They:

  • drop the object containment;
  • make either bound strict;
  • drop either bound;
  • count elements as bytes;
  • discharge validity without the containment;
  • contain an argument with unknown origins in no object.

  The start-bound mutant at first survived; the trusted before case now kills it.

• Docs: check-doc-examples.py passes on every page this changes (62 examples, 10 against the verdicts their pages show).

• Merges: this merges cleanly with each open PR, verify: Follow the body of a choose in a spec's reads and postcondition checks #43, verify: Make chooses with one condition one choice, kept across writes elsewhere #44, verify: Send crash reports to cpp-verify's issue tracker #46, and verify: Bound what a run builds and what its solvers allocate #48 to verify: Reach the fields and array elements of a record through a pointer #50.