Polyspace Code Prover incremental/delta analysis

Hi,

is there an option to run Polyspace Code Prover only for changes since the last baseline/commit (basically for files that only changed since the last baseline/commit) ?

This would be crucial to decrease analysis time.

The only adjusting screws for analysis time I know are precision level (-O0, -O1 etc.), verification level (pass0, pass1 etc.) and CPU core count (max-processes option).

We set up PSCP for now locally but the goal is to run it in the CI pipeline and shorter pipeline runs are of course preferred.

[Isha]

Hello,

The Code Prover performs formal analysis over all execution paths and inputs, which requires whole‑program reasoning rather than per‑file analysis Polyspace Code Prover - MATLAB

There is no documented incremental/delta analysis feature for Code Prover in documentation Polyspace Code Prover Documentation

The -incremental option exists, but only for Polyspace Bug Finder, not Code Prover -incremental - Enable incremental compilation during an analysis - MATLAB

As a result, we typically reduce CI time by:

• running Code Prover on modules/subsets of code (when possible), and
• using faster partial checks (e.g., Bug Finder or reduced precision) in PR pipelines, with full Code Prover runs scheduled separately.

Hope this helps.

Answer 1

[Angel]

是的，但没有一个内置的“一键只分析变更文件”选项。通常会在 CI 流程中通过 git diff 识别自上次基线/提交以来修改过的文件，然后仅对这些文件或模块运行 Polyspace。与此同时，仍建议定期执行完整分析。

-incremental 选项确实存在，但仅适用于 Polyspace Bug Finder，不适用于 Code Prover。对于 Code Prover，如果想减少分析时间，通常需要通过 CI 流程结合 git diff 等方式，仅对变更的文件或模块执行分析 -incremental - Enable incremental compilation during an analysis - MATLAB Geometry Dash