How do I configure a Git repository which contains a Polyspace project?

I am running Polyspace R2022a inside a Git repository, such that both the Polyspace project and the code under analysis are contained in the repository.

I want to configure the Git repository such that all users, even those with fresh clones of the repository, can do the following:

1) Run Polyspace over the source code with identical configuration and including justifications added by other team members.

2) Add new justifications and have them merge into Git along with the source code.

One obvious approach is to take all files generated by Polyspace and check them into Git. This technically satisfies the above requirements, but is highly inconvenient: running Polyspace causes large changes to the Git repository, which clutters any code changes and causes frequent merge conflicts.

How do I configure the Git repository such that points (1) and (2) are satisfied, while checking as few files as possible into Git?

Answer 1

[MathWorks Support Team]

In Polyspace, justifications are stored as part of the folders which contain details of the last Polyspace run. These are the folders named "<module name>/CP_Result/" or "<module name>/BF_Result/" (for Polyspace Code Prover or Polyspace Bug Finder, respectively). Polyspace uses the information in these folders to re-use justifications between runs, even when code is modified or moved. If these folders are removed, Polyspace will start again and the justifications will be lost.

Polyspace does not support partially checking these folders into Git. Therefore, the only way to preserve justifications that were added using Polyspace's Graphical User Interface is to check all contents of result folders into Git.  As you observed, this causes large changes in the Git repository every time Polyspace is run.

A possible workflow is to add the justifications directly into the source code as formatted comments, known as 'annotations'. For example, the following annotation will justify a division-by-zero check:

int main(void) {
  int x = 0;
  int y = 1 / x; // polyspace RTE:ZDV Replace this comment with the justification reason
  return 0;
}

If all justifications are stored within the source code, then the Git repository can be configured in two steps:

1) Fully ignore the files generated by Polyspace, by adding the following lines to the .gitignore file:

*/CP_Project/
*/BF_Project/

2) Make sure to check Polyspace's project (.PSPRJ) file to the Git repo. This defines which source files are analyzed and will not change often.

Documentation on Polyspace code annotations can be found here:

https://www.mathworks.com/help/releases/R2022a/bugfinder/ug/annotate-hide-known-acceptable-polyspace-results-web-browser.html

A table of acronyms used by Polyspace Code Prover can be found here:

https://www.mathworks.com/help/releases/R2022a/codeprover/ug/check-acronyms-for-code-comments.html