Skip to content

feat: AUTOSAR Classic Platform C rule pack + Coverity import bridge + CBMC proof coverage #66

Description

@SoundMatt

Summary

Depth-track roadmap item (2026-07-27). Implements this repo's share of the common schemas defined in SoundMatt/FuSaOps#78 (spec RFC — read that first; this issue only covers c-FuSa-specific implementation, not the wire format itself).

1. AUTOSAR Classic Platform C rule pack

The x-FuSa spec already reserves the AUTOSAR-* rule-id prefix (§1.5.1) — it's just never been implemented. Add a cfusa autosar command mirroring the existing cfusa misra command, implementing a starter set of AUTOSAR Classic Platform C rules. Only add rules that are genuinely AUTOSAR-specific (e.g. naming conventions, memory-partition rules, specific banned-API lists) — check against the existing MISRA-C rule set first and skip anything already covered by cfusa misra/cfusa lint, to avoid duplicate findings for the same defect under two different rule IDs.

2. Qualified-tool bridge (Coverity import, per FuSaOps#78 §A)

cfusa check --import <path> --import-format coverity

Implement the Coverity decoder first per the RFC's MVP recommendation — it's the cleanest JSON export of the four external tools discussed. Reuse the existing Finding/fingerprint machinery unchanged; only the decoder (Coverity JSON → Finding[]) and the --import/--import-format flag parsing are new. Set tool: "coverity" on imported findings (not "cfusa") so aggregated output can distinguish native from imported.

3. Formal-verification proof coverage (CBMC, per FuSaOps#78 §B)

cfusa coverage --proof --proof-file <cbmc-xml-output> --proof-threshold N

Parse CBMC's --xml-ui output and emit proof-report.json in the exact shape specified in FuSaOps#78 §B, with tool: "cbmc". This schema is the one ada-FuSa will later need to match exactly for gnatprove — get it right here first since it's lower-stakes to iterate on now than after ada-FuSa exists.

Suggested order

CBMC proof coverage first (derisks the Ada roadmap item), then Coverity import, then AUTOSAR rules (lowest risk, most mechanical — same pattern as the existing misra command).

Reference: SoundMatt/FuSaOps#78

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions