Read a report

--checked-report=path computes contracts and writes JSON without selecting additional functions. Compiler spelling: -fweavec-checked-report=path.

Version 2 contains the invocation result, tool/model versions, totals and units with source, target and function records. Each function records:

• selected, complete, deferred, and limited flags;
• status: proven, conditional, trusted, or incomplete;
• sufficient requirements and guaranteed establishes, including when input guards and optional on returning outcomes;
• obligations with property, outcome, source location, reason and call origins;
• case_inputs, the optional candidate input paths, and cases, each with canonical premises and its own complete contract and obligation ledger.

Case results do not change the generic function’s status or the totals of selected definitions. Selecting both a successful caller and its incomplete generic helper still fails the invocation. Compact reports preserve the same case records when expanded with scripts/checked-report.py.

Obligation outcomes distinguish proven facts, entry requirements, explicit trust, unresolved coverage and violations. A complete conditional helper still requires its caller to establish the exported preconditions. Trust in WEAVEC_UNSAFE, WEAVEC_ASSUME, declared annotation assumptions and modeled library contracts propagates to callers and remains visible. A trust marker alone does not supply missing storage facts; modeled effects and complete postconditions still govern subsequent checks. The trusted status can also carry entry requirements; callers still need to establish them. invocation_ok: false means the command did not establish its requested result, even if an independent function has a complete contract.

Reports are deterministic for identical inputs and are replaced atomically. They are also written on checked failures. A report output error fails the invocation instead of leaving a successful status without the requested result.

Memory contracts can name dereferenced parameters, record fields, selected elements, globals and result paths. Requirements distinguish validity, extent, initialization, writability, release family, separation, string termination and nonoverflowing byte sums. initialized and zeroed postconditions establish byte intervals; copied preserves only the input bytes already initialized within an interval. It does not claim that unused input capacity was initialized or that the bytes retain a particular value.

Traversal contracts additionally use position for an output pointer’s inclusive byte-displacement interval from a captured entry pointer. progress relates two cursors’ advances from their respective entry values; it preserves a caller’s proved order without equating unrelated arrays. An endpoint such as terminator param 0 scale 1 plus 0 names the selected entry witness’s byte index. It is not a C integer argument or an exact strlen result. Entry terminated requirements use begin for the minimum witness index; their end is zero. A terminated output uses begin for the initialized prefix start and end for the known zero byte. Input values are captured before a call overwrites their holders, and conditional outputs apply only on their recorded outcomes.

These facts use summary format 17, sidecar format 18 and checked-record encoding 4. Expanded JSON remains version 2; compact JSON remains version 3.