Polyspace

MathWorks Polyspace comes in two flavours — Code Prover (sound abstract interpretation, proves absence of runtime errors) and Bug Finder (faster, finds defects without full soundness). Roboticks ingests both via the same connector.

v1 sync modes: CLI push (primary) for desktop / CI Polyspace, plus REST cloud sync for Polyspace Access deployments. The adapter auto-detects the mode based on base_url — point at a Polyspace Access URL and it talks REST; point at a local results folder and it reads JSON files.Code Prover proofs (proven Run-Time Error free) land as status=pass evidence with source_type=polyspace_runtime_proofs — that’s the high-signal evidence that maps directly to safety requirements.Tool-qualification preservation: every Polyspace-sourced evidence row is marked qualified_artifact=true. AI triage skips these rows; evidence packs preserve the raw JSON/XML byte-exact for ISO 26262 / DO-178C audit.Cloud sync availability: Polyspace Access cloud sync requires MathWorks Connections partnership to be active for your organization. Until then, CLI push covers all cases.

Connector type and pricing


Type	BYO static-analysis connector
Tier	Team (3 BYO connectors included), Enterprise (bundled)
Price	$149 / connector / month above the Team allowance
Polyspace license	You bring it. Roboticks ingests reports; we don’t run Polyspace.

What ingests

Polyspace tool	Source command	Lands in Roboticks as
Code Prover results (`polyspaceCodeProver`)	`polyspace-results-export -format xml`	`finding` (per-check: Color, Severity, Verification result)
Bug Finder results (`polyspaceBugFinder`)	`polyspace-results-export -format xml`	`finding` (per-defect: Category, Detail)
MISRA C/C++ rule checks	included in either run	`finding` (rule violations)
Coding-rule / coverage metrics	`polyspace-results-export -format xml -coverage`	`metric` (per-source-file)

Wire it in (v1 CLI push)

Subscribe in Roboticks

Settings → Integrations → Static analysis → Polyspace → Subscribe.

Run Polyspace and export results to JSON

Code Prover:

polyspaceCodeProver -options-file ./polyspace.opts \
                    -results-dir ./psp-results
polyspace-results-export -results-dir ./psp-results \
                         -format json \
                         -output-file ./psp-results/results-CP-${BUILD_ID}.json

Bug Finder:

polyspaceBugFinder -options-file ./polyspace.opts \
                   -results-dir ./psp-bf-results
polyspace-results-export -results-dir ./psp-bf-results \
                         -format json \
                         -output-file ./psp-bf-results/results-BF-${BUILD_ID}.json

Configure and sync

rbtk connector configure polyspace \
    --results-dir=./psp-results \
    --tool-version=R2024b \
    --qualification-kit-version=2024-DOAQK \
    --label=primary --project-slug=flight-controller

rbtk connector sync polyspace --label=primary

The adapter reads all *.json files under the configured directory. Bug Finder findings land as fail evidence; Code Prover proofs (color: green or category in OVFL/OOB/ZDIV) land as pass evidence with source_type=polyspace_runtime_proofs — exactly the high-signal artifact safety auditors want to see.

Cloud sync (Polyspace Access, post-Connections)

If your team runs Polyspace Access (the self-hosted web UI) AND your organization has MathWorks Connections partnership active, you can configure cloud sync:

rbtk connector configure polyspace \
    --url=https://polyspace.acme.internal \
    --auth=pat \
    --token=$POLYSPACE_ACCESS_TOKEN \
    --polyspace-project-id=fc-2024 \
    --label=primary --project-slug=flight-controller

The adapter auto-detects Access mode from the URL shape and uses the REST API at /api/v1/projects/{id}/runs + /api/v1/runs/{id}/findings. Incremental sync via modified-after={cursor}.

CI recipe

# .github/workflows/polyspace.yml
name: Polyspace
on: { push: { branches: [main] }, pull_request: {} }

jobs:
  polyspace:
    runs-on: [self-hosted, polyspace-licensed]
    permissions: { id-token: write, contents: read }
    steps:
      - uses: actions/checkout@v4

      - name: Polyspace Code Prover
        run: |
          polyspaceCodeProver -options-file polyspace.opts \
                              -results-dir psp-results
          polyspace-results-export -results-dir psp-results \
                                   -format xml \
                                   -output-file psp-cp.xml

      - name: Polyspace Bug Finder
        run: |
          polyspaceBugFinder -options-file polyspace.opts \
                             -results-dir psp-bf-results
          polyspace-results-export -results-dir psp-bf-results \
                                   -format xml \
                                   -output-file psp-bf.xml

      - run: pipx install roboticks-cli
      - run: rbtk auth oidc-from-github

      - run: |
          rbtk findings upload --tool polyspace \
            --label branch=${{ github.ref_name }} \
            psp-cp.xml psp-bf.xml

Defect mapping

Code Prover color → Roboticks severity

Color	Meaning	Roboticks severity
Red	Definite runtime error	`critical`
Orange	Possible runtime error	`error`
Green	Proven safe	suppressed (passes recorded as `coverage`)
Gray	Unreachable code	`warning`

Bug Finder categories → Roboticks severity

Polyspace category	Roboticks severity
Defect → High impact	`critical`
Defect → Medium impact	`error`
Defect → Low impact	`warning`
Coding standard violation (MISRA Required)	`error`
Coding standard violation (MISRA Advisory)	`warning`

Override at Settings → Findings → Severity mapping.

Where findings appear

Traceability matrix — Polyspace findings for a source file appear on every requirement whose @confirms-annotated test exercises that file. The cell shows a finding badge.
Requirement detail — Per-requirement view lists findings under Static analysis findings (Polyspace), with separate sub-sections for Code Prover and Bug Finder.
Release evidence pack — A Polyspace appendix in the PDF lists open Reds, Oranges, and unjustified Bug Finder defects, with the raw XML reports in the ZIP.
PR Check Run — Roboticks · Polyspace with new/resolved findings delta vs the base ref.

Justifications

Polyspace’s Review status (justification, comment) round-trips:

polyspace-results-export -results-dir psp-results \
                         -format xml \
                         -with-review-info \
                         -output-file psp-cp.xml

Roboticks reads the <review> block. Defects marked Justified or No Action Planned are suppressed from gating logic and shown as muted in the UI.

Gating

# .roboticks/findings-policy.yaml
polyspace:
  block_pr_if:
    new_code_prover_red: > 0
    new_bug_finder_high: > 0
    new_misra_required: > 5

Coverage from Code Prover proofs

A unique Code Prover output is proof coverage — the fraction of operations that were proven Green. Roboticks treats this as a coverage metric (alongside test coverage) so a release can be evaluated against, e.g., ”≥ 99% of pointer dereferences proved Green”.

# .roboticks/findings-policy.yaml
polyspace:
  require_proof_coverage:
    pointer_dereferences: ">= 99%"
    array_accesses: ">= 99%"

Troubleshooting

`Unsupported Polyspace XML schema version`

Roboticks targets the schema from Polyspace R2022a and newer. For R2021b and older, post-process with the XSLT MathWorks publishes in the Polyspace docs, or upgrade.

Findings don't link to a requirement

Polyspace findings link via source file. Files not exercised by any @confirms-annotated test land under Unlinked findings. Add a test that imports/exercises the file with a @confirms("REQ-...") annotation.

Polyspace results too large to upload

The CLI streams the XML; there is no upload size cap, but a ~500 MB report takes a few minutes. Use --gzip to compress the upload payload.

LDRA

The other heavyweight C/C++ static-analysis tool.

Coverity

Black Duck Coverity for broad-language analysis.

Quick Start

GitHub App

Requirements

Traceability

Testing

SDK

Self-Hosted Runners

AI Features

CLI

Evidence Packs

Standards Coverage

Compliance Patterns

Integrations

Pricing

Resources

Polyspace

Polyspace

Connector type and pricing

What ingests

Wire it in (v1 CLI push)

Cloud sync (Polyspace Access, post-Connections)

CI recipe

Defect mapping

Code Prover color → Roboticks severity

Bug Finder categories → Roboticks severity

Where findings appear

Justifications

Gating

Coverage from Code Prover proofs

Troubleshooting

Next

LDRA

Coverity

​Polyspace

​Connector type and pricing

​What ingests

​Wire it in (v1 CLI push)

​Cloud sync (Polyspace Access, post-Connections)

​CI recipe

​Defect mapping

​Code Prover color → Roboticks severity

​Bug Finder categories → Roboticks severity

​Where findings appear

​Justifications

​Gating

​Coverage from Code Prover proofs

​Troubleshooting

​Next

LDRA

Coverity

Polyspace

Connector type and pricing

What ingests

Wire it in (v1 CLI push)

Cloud sync (Polyspace Access, post-Connections)

CI recipe

Defect mapping

Code Prover color → Roboticks severity

Bug Finder categories → Roboticks severity

Where findings appear

Justifications

Gating

Coverage from Code Prover proofs

Troubleshooting

Next