[SwayamInSync]

Stacked on #68 (LM1b, on #67, #66, #65, #62, and #63), whose commits show here until they merge; merge after #68.

One construct the verifier does not represent stopped the whole file: its error was printed and no function of the file was verified. On the base, for a file with a switch in pick, a function inc that is fine, and a caller user of pick:

two.cpp:4:3: error: pick: unsupported statement: SwitchStmt
    4 |   switch (x) {
      |   ^~~~~~~~~~~~

and nothing else, exit status 1. Now the error is the same and costs pick alone:

two.cpp:4:3: error: pick: unsupported statement: SwitchStmt
    4 |   switch (x) {
      |   ^~~~~~~~~~~~
Verified: inc [backend=z3]
Unresolved: user [backend=z3] [reason=callee.contract] (relies on the contract of pick (it uses a construct the verifier does not support), which is not established)

Design

Decided for 0.2 (E1): an unsupported construct affects only its function; the function is Unresolved [reason=construct.unsupported] with the located message, callers relying on its contract are demoted through the existing fixpoint, users of a spec that failed to convert are demoted too, every other function is verified, and the exit status stays non-zero (Q5).

• References. Kani and CBMC turn a construct they do not translate into a check that fails where it is reached (codegen_unimplemented), so only what reaches it is affected; Prusti and Creusot report an unsupported feature as an error for its function and verify the others. Frama-C, Dafny, and Verus stop at a front-end error. cpp-verify keeps the error as Clang prints it, as Prusti does, and gives the function its verdict.
• Attribution. Every error of the converter records the function it is raised in and whether it was in the signature and contract (ConversionError::InContract) or the body. The errors that passes after conversion find about one function (a recursion without a measure, a mutual recursion without a shared measure, a malformed inductive predicate) belong to it too (errorOf; the inductive pass now reports the predicate). So do the two translation-unit errors about functions (a contracted member function, a function template). An error of no function still stops the run.
• What remains (markUnsupported, VFunction::UnsupportedConstruct), what others may rely on:
  • an executable or proof function whose contract converted becomes an external contract with its body cleared, as a contract without a definition is: its callers are verified against it and demoted (callee.contract, "it uses a construct the verifier does not support"), and the calls of its body are unverified callers of their callees;
  • one whose contract did not convert is left out, and a call of it is already an unsupported obligation where it is ("a call of lookup, whose contract is not available");
  • a spec, written or a lifted constexpr helper, becomes a declaration without its definition, postconditions, reads, domain, or unfolding, which nothing may assume. A function whose SpecDependencies (bodies, contracts, callees' contracts) reach it is not verified at all: Unresolved [reason=construct.unsupported] ("relies on choice, which uses a construct the verifier does not support"). A proof modulo an uninterpreted spec would be sound, but none of its counterexamples could be checked, and this reason names the cause.
• The converter now returns a spec whose body failed (the axiomatization check, an empty body after a rejected statement) instead of null, so it can be declared.
• The driver prints every error as before, in the order before; the first error of each function carries its verdict, so its JSON record is "status":"unresolved", "reason":"construct.unsupported" with the range, and every error names its function. A translation unit whose functions are all unsupported still exits 1 (the first version returned success there with "no verifiable functions found"; z3_types_fail_closed.cpp and two other tests caught it).
• Ownership inference treats such a function as external, as any external contract.

Assertions build

The first CI run's Linux assertions job failed 32 tests on GlobalDecl::Init: Use other ctor with dtor decls!: the errors of member functions now name their function by its identity, which mangles it, and functionIdentity built GlobalDecl(FD) for every function, a constructor or destructor (the implicit ones of a record) included, which a release build mangles without the check. A constructor or destructor is now mangled as its complete-object variant (Ctor_Complete, Dtor_Complete); the identities of every other function are unchanged. The 32 tests pass on an assertions build.

Windows

The Windows smoke test failed. Its program includes <filesystem> and <vector>, and naming the errors of templates and member functions mangled every one in the translation unit, the headers' included, before asking whether it had contracts to report. Microsoft's mangler cannot mangle a dependent type (cannot mangle this dependent-length yet, cannot mangle this template specialization type yet), so every run under the MSVC target stopped with those errors. Only a template or member function with contracts, the one that is reported, is now named. microsoft_identity.cpp verifies a function beside an uncontracted function template with a dependent array length, a class template's member, and a plain member, under --target=x86_64-pc-windows-msvc; on the base it fails with two cannot mangle errors.

Tests

suite/per_function_errors.test, on Inputs/per_function_errors.cpp, with Z3, JSON, BMC, and Lean export:

• pick (a body with a switch) and its caller uses_pick: callee.contract;
• lookup (a precondition reading a global array) and its caller: the call is construct.unsupported;
• choice (a spec with a switch), a function whose postcondition applies it and a lemma about it: both construct.unsupported, "relies on choice";
• zero_lemma (a proof function with a switch) and a function that calls it in a ghost block: callee.contract;
• step (an uncontracted constexpr helper with a switch) and its caller: construct.unsupported;
• inc, twice, and uses_twice verify as before; no unsupported function gets a verdict of its own;
• JSON: the first error's record carries the verdict and the range, the second error of lookup names it, and the other verdicts are as in text;
• BMC and a Lean export verify or export the same functions.

located_errors.cpp now also checks the records of pick and of down (a recursion without a measure, found after conversion), which carry their verdicts.

Mutants, each built and run on per_function_errors.test, located_errors.cpp, z3_types_fail_closed.cpp, deep_expressions.test, and object_layout_array_fails_closed.cpp: 10 of 10 killed.

Mutant	Killed by
every error stops the file	per_function_errors
a body error counts as a contract error	per_function_errors
an unsupported function keeps its body (verified as it is)	per_function_errors
an unsupported spec keeps its definition	per_function_errors
users of an unsupported spec are verified	per_function_errors
callers rely on an unsupported function's contract (taken as trusted)	per_function_errors
the first error carries no verdict	per_function_errors, located_errors
errors after conversion belong to no function	located_errors
a file of unsupported functions succeeds	z3_types_fail_closed, deep_expressions, object_layout_array_fails_closed
only the first error names its function	per_function_errors, located_errors

Docs

• tooling.rst: the unsupported construct example, now beside a verified function and a demoted caller (checked by docs_examples.test); what others may rely on; the JSON record.
• limitations.rst: failing closed per function.
• ch16: construct.unsupported for a function the verifier does not represent and for its users.
• Release notes: "An unsupported construct costs its function alone".
• DESIGN.md, ARCHITECTURE.md: the design above.

Open

• A lifted constexpr helper rejected before its body (an aggregate return, an unsupported parameter type) has no declaration: a user of it ends encoding.failed ("missing spec definition"), fail-closed, but without naming the cause.

Checked

• The Verify suite on a release build: 451 passed, 1 unsupported (the exhaustive decoder), 1219 s with 32 workers; docs_examples.test checks the new tooling example.
• per_function_errors.test on the base: the file stops after its errors, with no verdict.
• After the Windows fix: microsoft_identity.cpp, template_contracts.cpp, and located_errors.cpp pass on an assertions build of this branch, and the first fails on the base.