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:
A table of acronyms used by Polyspace Code Prover can be found here:
