[SwayamInSync]

Plan item E7 (verification inside clang++ builds): a compilation verified every file with the defaults (Z3, 30 s a query, one job) whatever it needed, and every file without contracts warned, so a build that gave -fverify-contracts to every file printed a warning for most of them.

On the base

$ clang++ -std=c++17 -fverify-contracts -c plain.cpp -o plain.o      # int add(int a, int b) { return a + b; }
warning: no verifiable functions found [-Wcppverify]
1 warning generated.
$ clang++ -std=c++17 -fverify-contracts -fverify-timeout=5000 -c ok.cpp -o ok.o
clang++: error: unknown argument: '-fverify-timeout=5000'

With this PR

Option	Meaning (the cpp-verify option)
-fverify-backend=z3|cvc5|portfolio|race|bmc	the solver (--backend); Lean projects stay with cpp-verify
-fverify-timeout=<ms>	each query's time (--timeout, 30000 by default, 0 disables); collections get twice it and a function ten times it, as with cpp-verify
-fverify-jobs=<n>	solver jobs for each compilation (--jobs), 1 by default, since a build compiles several files at once
-fverify-cache=<dir>	proofs kept in <dir> (--proof-cache), shared by every compilation that names it
-fverify-report, -fverify-report=<file>	the results as JSON Lines (--diagnostics-format=json), ending with the summary record, in <object>.cppverify.json beside the object or in <file>

$ clang++ -std=c++17 -fverify-contracts -Rcppverify -fverify-report -c ok.cpp -o ok.o
ok.cpp:2:5: remark: Verified: inc [backend=z3] [-Rcppverify]
$ cat ok.o.cppverify.json
{"backend":"z3","function":"inc","function_source":{...},"message":"inc [backend=z3]","schema":"cppverify.diagnostic/2","severity":"note","status":"verified"}
{"bounded_safe":0,"exported":0,"failed":0,"interrupted":0,"lowered":0,"reasons":{},"schema":"cppverify.summary/1","trusted":0,"unresolved":0,"verified":1}
$ clang++ -std=c++17 -fverify-contracts -c plain.cpp -o plain.o
$ clang++ -std=c++17 -fverify-contracts -fverify-backend=lean -c ok.cpp -o ok.o
error: invalid value 'lean' in '-fverify-backend=lean'

A file without a function to verify says nothing (cpp-verify still warns for one: a run asked to verify it).

Design

• Clang's own options. The options are FrontendOptions fields parsed by Clang's option marshalling (MarshallingInfoEnum for the backend, MarshallingInfoInt for the numbers), so an invalid value is the compiler's usual error, and the driver forwards them as it forwards -fverify-contracts-out=.
• A report per object, as -ftime-trace does. In a build the same flag goes to every file, so a bare -fverify-report writes <object>.cppverify.json beside each object: the driver, which knows the output, passes -fverify-report=<path> to the compiler, as -ftime-trace names its file after the object. The report is the records cpp-verify --diagnostics-format=json prints, then the summary record; the summary record is built in one place now (summaryRecord), which cpp-verify uses too.
• The tool's meaning for the tool's names. compilationOptions maps the options as cpp-verify maps --timeout, --jobs, --backend, and --proof-cache, including the timeouts a query timeout scales. The proof cache already writes atomically and prunes once per run, so compilations may share a directory.
• Quiet on success. A proof is a remark (E3); with QuietWithoutFunctions a file without contracts is no longer a warning.
• The upstream hook stays one line: CodeGenAction passes the FrontendOptions instead of one field.

Tests

• compile_options.cpp (new): the driver forwards every option and names a bare -fverify-report's file after the object, or keeps the file given; an invalid backend or timeout is the compiler's error; a file without contracts compiles with no output at all (count 0); -fverify-backend=bmc reaches the verifier ([backend=bmc, bound=0]), with a proof and a failure, and -fverify-report= holds both records and a summary of one verified and one failed; -fverify-cache= fills the directory.
• CompilationOptionsTest (new, VerifyTests): the defaults, which must equal cpp-verify's own, each option, every backend, -fverify-timeout=0 disabling every limit as --timeout=0 does, and the extremes (0 jobs is 1; a timeout too large to scale gives no collection and function bounds, as cpp-verify).

On the base compile_options.cpp fails at its first option (unknown argument), and the file without contracts warns.

On a release build of this branch, the whole Verify suite passes (505 of 506, one unsupported) once a stale BUG_REPORT_URL in the local CMake cache is cleared; with it crash_report_url.cpp names LLVM's tracker, which a fresh configure, as CI's, does not.

Mutants

Each mutant below, applied alone and rebuilt, is caught (10 of 10):

Mutant	Change	Caught by
E1	-fverify-jobs is not forwarded	compile_options.cpp
E2	a bare -fverify-report is not named after the object	compile_options.cpp
E3	a file without functions warns	both
E4	the report is not written	CompilationOptionsTest
E5	the report has no summary record	compile_options.cpp
E6	bmc verifies with Z3	both
E7	the timeout is not applied	CompilationOptionsTest
E8	the jobs are not applied	CompilationOptionsTest
E9	the cache is not applied	both
E10	a zero timeout keeps the default	CompilationOptionsTest

Review also found that -fverify-timeout=0 first meant the default, where cpp-verify --timeout=0 disables the limit; the option now defaults to 30000 and 0 disables, as for the tool.

Docs

• Tooling: "Options of a compilation" (the table, the errors, the quiet file) and "Verification in a CMake build", a recipe with -fno-verify for development builds;
• the toolchain chapter: "Verification in a build";
• release notes; ARCHITECTURE (Compile-Time Integration).

Not done

• -fverify-* options for the Lean backend, and for --function or --max-failures: a compilation verifies the whole file with a solver.
• A cache of whole functions' results (C8): the cache keeps proofs of single obligations, so an unchanged file is not free, only cheaper.