[SwayamInSync]

valid(p, n) declares an extent only as a top-level condition of a precondition, where memory checking reads it. Anywhere else it lowered to its builtin spec, whose body is true, so a claim made with it held without meaning anything. On 0.1.1 and main this verifies:

int *start_of(int *buf)
  cv::pre(valid(buf, 4))
  cv::post(valid(cv::result, 4))
{
  return nullptr;
}

Verified: start_of [backend=z3]

The change: under --check-ub, misplacedValidMarker (Transform/UBChecks.cpp) looks for the marker everywhere else a function may state a condition: postconditions, recommends, decreases, cppverify::when, the proof blocks of a spec's clauses, loop invariants, measures, and footprints, cppverify::check, assumptions, and ghost code. It also checks spec functions, whose bodies instrumentUBChecks does not visit. A marker found there is an error for that function, which is then not verified; the other functions of the file still are:

error: start_of: valid(p, n) declares an extent only as a top-level condition of a cppverify::pre, and has no meaning in a postcondition

The message ends with the place: a postcondition, a loop invariant, a cppverify::check, ghost code, or a spec function. A user-declared spec named valid is the same marker and gets the same check. With --no-check-ub every marker already folds to true with a warning, and none is an error.

Docs:

• the syntax table says where the marker may appear;
• the pointers page gains a section with the rejected example, its exact error, and what to write instead (relate a result to a parameter whose extent callers know; an invariant does not repeat the precondition's extent);
• the limitations page says no extent can be stated for a returned pointer yet;
• DESIGN and ARCHITECTURE describe the check;
• the release notes get an entry under "Wrong results fixed".

Testing: Verify/suite/valid_outside_precondition.cpp covers a marker in a postcondition, a loop invariant, a cppverify::check, ghost code, and a spec function, each an error naming its place. A function that uses the marker correctly still verifies, and under --no-check-ub the warning appears and in_post verifies. It fails on main. Each of five mutations fails it: not checking postconditions, loop invariants, cppverify::check, ghost code, or spec functions. The documentation's rejected example also fails against main's binary, which accepts it.

Checked: Verify suite 424 passed, 1 unsupported; VerifyTests 60 passed, 1 skipped (encoding parity, which needs archives). A verdict differential against main over 432 Verify sources changes only the new test. After the rebase onto #39, every documentation example passes (175) and the site builds with -W.