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

> Bring your MathWorks Polyspace license. Roboticks ingests Code Prover and Bug Finder report XML and surfaces results in the traceability matrix and evidence pack.

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

<Info>
  **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.
</Info>

## 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)

<Steps>
  <Step title="Subscribe in Roboticks">
    **Settings → Integrations → Static analysis → Polyspace → Subscribe**.
  </Step>

  <Step title="Run Polyspace and export results to JSON">
    Code Prover:

    ```bash theme={null}
    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:

    ```bash theme={null}
    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
    ```
  </Step>

  <Step title="Configure and sync">
    ```bash theme={null}
    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.
  </Step>
</Steps>

## 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:

```bash theme={null}
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

```yaml theme={null}
# .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:

```bash theme={null}
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

```yaml theme={null}
# .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".

```yaml theme={null}
# .roboticks/findings-policy.yaml
polyspace:
  require_proof_coverage:
    pointer_dereferences: ">= 99%"
    array_accesses: ">= 99%"
```

## Troubleshooting

<AccordionGroup>
  <Accordion title="`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.
  </Accordion>

  <Accordion title="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.
  </Accordion>

  <Accordion title="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.
  </Accordion>
</AccordionGroup>

## Next

<CardGroup cols={2}>
  <Card title="LDRA" icon="microscope" href="/integrations/ldra">
    The other heavyweight C/C++ static-analysis tool.
  </Card>

  <Card title="Coverity" icon="microscope" href="/integrations/coverity">
    Black Duck Coverity for broad-language analysis.
  </Card>
</CardGroup>