[SwayamInSync]

--diagnostics-format=json was the only machine-readable output, and it left out what an editor or a CI system needs (findings F5 and R5 of the 0.2 plan):

• A verified, vacuous, partial, callee.contract, or unsupported result carried no location at all.
• A failure's source began at the check's caret and ended at the first column of its last token. For cv::post(cv::result >= 0) it was columns 23 to 26, >= 0, so a viewer underlined the operator and its right operand, not the expression.
• Compiler errors were text on stderr, even in JSON mode.
• No record ended the run.
• There was no SARIF from cpp-verify (E3 gave the compiler path SARIF through Clang's own writer) and no GitHub annotation.

This is plan item E6, stacked on #104 (E3).

JSON Lines: cppverify.diagnostic/2

On structured_output.cpp of the new test, --diagnostics-format=json now prints:

{"message":"using the result of an assignment as a condition without parentheses","option":"-Wparentheses","related":[{"message":"place parentheses around the assignment to silence this warning","source":{"column":9,"end_column":9,"end_line":26,"file":"structured_output.cpp","line":26}},...],"schema":"cppverify.diagnostic/2","severity":"warning","source":{"column":7,"end_column":12,"end_line":26,...},"status":"frontend"}
{"backend":"z3","function":"inc","function_source":{"column":5,"end_column":8,"end_line":3,...},"message":"inc [backend=z3]","schema":"cppverify.diagnostic/2","severity":"note","status":"verified"}
{"backend":"z3","counterexample":"x = -2, result = -1","function":"clamp","function_source":{...},"message":"verification failed: clamp [postcondition] [backend=z3] [reason=counterexample]","model":[...],"obligation":{"id":"...::postcondition@11:23","kind":"postcondition",...},"reason":"counterexample","schema":"cppverify.diagnostic/2","severity":"error","source":{"column":12,"end_column":27,"end_line":11,...},"status":"failed","trace":[{"active":true,"kind":"branch","message":"then",...,"text":"takes the true branch"},...]}
...
{"bounded_safe":0,"exported":0,"failed":1,"interrupted":0,"lowered":0,"reasons":{},"schema":"cppverify.summary/1","trusted":0,"unresolved":0,"verified":2}

• function_source. Every record of a function, conversion errors included, names where the function is declared.
• source. A failure's source is the expression its check checks, from its first character to the column after its last, as SARIF and editors count. The anchor (the caret) stays in obligation.id.
• Rendered text. A failure gives counterexample and each trace step's text exactly as the text output prints them.
• Compiler diagnostics. The compiler's own diagnostics are records of status frontend, with their -W option and the notes that follow them as related. They come before the verifier's records of their file.
• Summary record. A cppverify.summary/1 record ends the run with the counts of the text summary.
• No times. No record holds a time, so the stream stays identical at any --jobs; parallel_functions.test diffs it. --time-report adds cppverify.time/1 records.

SARIF 2.1.0

--diagnostics-format=sarif writes the same records into a buffer and translates them into one log when the run ends (sarifLog in Driver/StructuredOutput.cpp), so the two formats cannot disagree. The mapping follows Frama-C's markdown-report SARIF generator, which turns every property status into a result:

Result	SARIF kind	level	rule
failure	fail	error	the failing check's kind (postcondition, overflow, ...)
unresolved, interrupted	open	error	unresolved, interrupted
bounded-safe	open	warning	bounded-safe
warning	fail	warning	warning
proof	pass	none	verified
trusted	review	none	trusted
compiler diagnostic	fail or informational	Clang's	frontend

Each result also carries:

• its location (the record's source and the function as a logical location);
• the counterexample in its message and in properties;
• the path as a code flow, each step at its line with its text;
• notes as related locations.

The run's properties hold the summary. Four logs validate against the official SARIF 2.1.0 schema (jsonschema, sarif-schema-2.1.0.json from oasis-tcs/sarif-spec) with no errors: the test's source run, its compiler error, inductive_counterexamples.cpp (12 results with loop notes), and an archive replay.

GitHub annotations

--diagnostics-format=github prints the text, and after each error and warning a workflow command:

::error file=summary.cpp,line=14,col=12,endLine=14,endColumn=34,title=cpp-verify%3A postcondition::verification failed: add_two [postcondition] [backend=z3] [reason=counterexample]%0Acounterexample: x = 3, result = 5

The file is relative to the working directory (the checkout, in a workflow). The data and properties are escaped as the runner requires.

Ranges, and archive schema v5

ObligationSource keeps its anchor (Line, Column), from which stable IDs are built. It gains BeginLine/BeginColumn from E3's BeginLoc, and its end is now the column after the last character (Lexer::getLocForEndOfToken, through the expansion range in a macro).

Verifier::sourceOf computes a source once for annotation and for the JSON fallbacks. cppverify.obligation/5 archives record the begin, so a replayed record has the same range, and still reads /4 to /1: their begin is the anchor and their end stays the first column of the last token.

Validation rejects a range whose begin lies after its anchor.

Tests

• suite/structured_output.test (new) checks:
  • JSON v2: record order and the frontend record with its related notes;
  • function_source, the failure's range, counterexample, and step texts;
  • the summary record, and a compiler error as a record;
  • SARIF: kinds, levels, rules, the code flow, the region, the invocation, and the summary property;
  • a replayed archive's range;
  • GitHub annotations with workspace-relative paths.
• obligation_archive.test:
  • replays a record written down to schema v4, and rejects a range that begins after its anchor;
  • its Python helper reads schema v5 and writes v4.
• 17 existing tests and the fidelity gate's helper (run_backend_fidelity.py, which now skips the summary record) move to cppverify.diagnostic/2: the schema string, exclusive ends, and keys that now sort between adjacent ones.

On the base, structured_output.test fails at its first check: there is no sarif or github value, and the compiler's warning is not a record.

Each mutant below, applied alone and rebuilt, is caught by structured_output.test, obligation_archive.test, or located_errors.cpp (23 of 23):

Mutant	Change
J1	no function_source
J2	ranges end at the first column of the last token
J3	ranges begin at the anchor
J4	no counterexample text
J5	no step text
J6	conversion errors lose their function's location
J7	no summary record
F1	notes are separate records, not related
F2	compiler records wait for the end of the file
F3	no warning option
F4	compiler diagnostics stay text in JSON
S1	a failure is open
S2	no code flows
S3	verdict messages lose their prefix
S4	the summary is no run property
S5	related locations are dropped
S6	a failure's rule is generic
G1	no annotations
G2	annotations name absolute paths
G3	annotation properties keep their colons
G4	annotations lose the counterexample
A1	archives drop range begins
A2	a range that begins after its anchor is valid

The whole Verify suite passes on a release build: in the full run 490 tests passed and the fidelity gate failed, because its helper rejected the summary record; with the helper fixed, the gate passes on its own (1 test unsupported).

Stacked on #104.