Skip to main content

Documentation Index

Fetch the complete documentation index at: https://docs.roboticks.io/llms.txt

Use this file to discover all available pages before exploring further.

​
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

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

​
What ingests

Polyspace toolSource commandLands in Roboticks as
Code Prover results (polyspaceCodeProver)polyspace-results-export -format xmlfinding (per-check: Color, Severity, Verification result)
Bug Finder results (polyspaceBugFinder)polyspace-results-export -format xmlfinding (per-defect: Category, Detail)
MISRA C/C++ rule checksincluded in either runfinding (rule violations)
Coding-rule / coverage metricspolyspace-results-export -format xml -coveragemetric (per-source-file)

​
Wire it in (v1 CLI push)

1

Subscribe in Roboticks

Settings → Integrations → Static analysis → Polyspace → Subscribe.
2

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
3

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

ColorMeaningRoboticks severity
RedDefinite runtime errorcritical
OrangePossible runtime errorerror
GreenProven safesuppressed (passes recorded as coverage)
GrayUnreachable codewarning

​
Bug Finder categories → Roboticks severity

Polyspace categoryRoboticks severity
Defect → High impactcritical
Defect → Medium impacterror
Defect → Low impactwarning
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

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.
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.

​
Next

LDRA

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

Coverity

Black Duck Coverity for broad-language analysis.