How to include another source file to Polyspace Code Prover analysis WITHOUT verifying this extra file?

How does the analysis in "Polyspace Code Prover" perform its analysis of a source file, regarding to its defined includes?

I work in an embedded project where we have one source file for each embedded function inside the system. My situation is that I would like to use one specific "header"'s real implementation to increase the quality of the source file currently being verified? DO NOTE that I would NOT like to verify that extra source file, it comes from a third part.

The intention is to use this implementation to offer the source file "under test" real (not stubbed) function implementations so values returned to the source in the analysis comes from the actual support function, not some random stub value.

I am running this automatically through a script using "polyspace-code-prover-nodesktop".

[Lorenz Mende]

I come from a similar situation, also working with files from a third party corp. Are you able to dynamically generate the sources file?

If yes, you may just filter the sources file on runtime before the analysis. In our project the analysis is automated via Jenkins and sources.txt is generated with a python file just before starting polyspace.

Answer 1

[Jatin]

Hi @Fredrik Ellis,

From what I understand, you want to run Polyspace Code Prover on a source file while using the real implementation of a header file, so that it ensures that the values returned during analysis come from the actual support functions.

To achieve this, you could write the implementation of the header file in a separate file and use the "Exclude paths" feature introduced in R2024a. This feature allows you to exclude specific files and folders from static analysis or testing.

You can learn more about the "Exclude paths" feature in Polyspace Code Prover by referring the documentation below:

https://www.mathworks.com/help/bugfinder/ref/excludepaths.html