QCP-v2.0.4

We are pleased to announce QCP v2.0.4. This release expands the C programs that QCP can verify and makes complex verification failures substantially easier to diagnose. It introduces a more complete C preprocessor, floating-point verification, pointer-offset reasoning, reusable verified strategies, and strategy-divergence diagnostics, alongside major improvements to branch-aware annotations, Given-based context propagation, and VC feedback.

What's New

Full Preprocessing and Project-Aware Includes

QCP's preprocessing pipeline now covers the C constructs commonly needed by real projects:

• nested #if, #ifdef, #ifndef, #elif, #else, and #endif;
• object-like and function-like macros in both C expressions and annotations;
• include guards and #pragma once;
• quoted and angle-bracket includes, relative paths, and nested header directories;
• efficient handling of repeated includes; and
• original file, line, and column locations in diagnostics and generated witnesses.

Projects can also load include paths from a compilation database:

--compile-commands <file>

This makes it easier to run QCP against an existing C build layout without duplicating its include configuration.

Actionable Strategy-Divergence Diagnostics

Symbolic execution now detects repeating strategy applications whose expressions continue to grow, and reports the responsible rule sequence before the process exhausts memory. Diagnostics include rule files and IDs, priorities, expression size and depth, the successful application count, and a recent application trace.

The shared safeguard can be configured with:

--strategy-application-limit <count>

The default is 4096. The option is available across the shared command-line configuration used by symexec, lsp, mcp, and StrategyCheck. Divergence and limit failures use the stable summary Strategy application did not converge; structured clients can read the detailed trace from errormessage.additional_info.

The detector distinguishes growing cycles from legitimate repeated applications. Regression coverage includes the Graham Scan strategy cycle, text and JSON diagnostics, and custom application limits.

New Verification Support

Floating-Point Verification

QCP v2.0.4 adds Flocq-based proof support and FloatLib.v for floating-point programs. Finite-value safety obligations can be selected explicitly:

--float-finite-vc
--no-float-finite-vc

The release also improves floating-point Rocq output, standardizes generated comparison names, and provides tutorial cases with their generated goals and proofs.

Pointer Offsets and Mixed Memory Layouts

pointer_offset is now a first-class assertion and strategy expression. It is supported throughout parsing, type inference, matching, unification, SMT translation, symbolic memory access, witness generation, Rocq output, and strategy soundness generation.

Pointer and mixed-array strategies use the same representation, making offset reasoning consistent from C annotations through the generated proof obligations.

Major Improvements

Branch-Aware Annotations and Multiple Loop Invariants

Branch-sensitive symbolic execution and annotation handling have been strengthened across complex control-flow cases.

• Improved branch destructuring, private and full branch joins, grouped assertions, branch clearing, and branch-state transitions.
• Improved multiple loop invariants, including many-to-one matching between symbolic branches and invariants.
• Added stronger validation for duplicate, missing, and unmatched branch annotations, with more accurate source locations.
• Expanded positive and negative regression coverage for switch fallthrough, assertion ordering, branch names, private conditions, and branch joins.

See the examples in QCP_examples/QCP_demos_tutorial/ for the updated annotation workflow.

Given, from, and of Handling

Handling of Given, from, and of annotations has been improved throughout symbolic execution. Given variables are preserved more consistently through assertions, expressions, branch transitions, and function calls. Function-call post-states also propagate the relevant context more reliably, improving relational specifications and multi-stage reasoning.

VC and Symbolic-Execution Feedback

QCP now detects more invalid branches, reducing the number of branches explored during symbolic execution and producing simpler verification conditions.

New Examples and Proof Libraries

Tutorials

QCP_examples/QCP_demos_tutorial/ is the new home for feature-oriented tutorials. It includes:

• the incremental swap_simple1, swap_simple2, and swap_simple3 walkthroughs;
• branch-control and multiple-invariant examples;
• Given annotation examples; and
• floating-point verification examples.

Each walkthrough includes the relevant C source, strategies, generated goals, automated and manual proofs, and goal checks.

Convex Hull Verification

A new verification development under QCP_examples/Applications_human/convex_hull covers Graham Scan, deduplicating Graham Scan, and Andrew's monotone chain. It includes point-array and safe-execution strategies; geometry, ordering, convexity, maximality, reversal, and monadic specification libraries; and the corresponding generated goals and proofs.

These examples also serve as realistic stress tests for the new strategy-divergence diagnostics.

Additional Improvements

• Improved return, entailment, safety, and assertion witness printing.
• Improved LSP and MCP assertion display and source-location reporting.
• Added structured JSON regression tests for lexer, preprocessor, and parser errors.
• Updated the SMT integration and regenerated affected proofs.
• Refreshed Flocq, ArrayLib, StoreAux, CommonAssertion, CNotation, MonadLib, ListLib, Makefiles, Rocq project files, and example runners.
• Improved the AI-assisted annotation and proof workflow, including proof grouping, worktree isolation, partial-result reuse, validation, and final proof-hygiene guidance.

Validation

The Windows v2.0.4 build was exercised against all 204 commands in run-example-windows.cmd with a 30-second per-command guard:

• 191 commands completed successfully.
• 3 convex-hull commands stopped with the expected strategy-divergence diagnostic instead of unbounded memory growth.
• 5 commands reported existing example search-path or dependency configuration issues.
• 5 commands exceeded the regression harness's 30-second limit; these are timing observations, not proof failures.

Additional regression checks passed for text and JSON divergence diagnostics, configurable strategy limits, structured error messages, and representative SLL, DLL, BST, and array examples.

Migration Notes

• Regenerated VCs may differ because of branch-control semantics, Given propagation, preprocessing, false-branch removal, pointer offsets, floating-point checks, builtin strategies, and SMT updates. Match proofs to the current goal semantics rather than old witness numbers.
• Feature demos have moved to QCP_demos_tutorial; update imports and commands to use SimpleC.EE.QCP_demos_tutorial.
• Keep C include paths (-I) and strategy/Rocq logical mappings (-slp) aligned. They serve different purposes and are not interchangeable. Compilation-database users can provide include paths with --compile-commands.
• Floating-point projects should select a finite-value policy explicitly and use the updated Flocq support.
• Increase --strategy-application-limit only for a known finite derivation. If the diagnostic shows a growing cycle, inspect and repair the reported rules instead.

For detailed proof-porting guidance, see Version_Log/V2-0-4.md.

Happy verifying with QCP v2.0.4!