MATLAB: Does Polyspace R2017b or later ignore the code annotations

Polyspace Bug FinderPolyspace Bug Finder ServerPolyspace Code ProverPolyspace Code Prover Server

Polyspace introduced a new format for code annotation syntax in R2017b. I have adapted my workflow to use this new format (see documentation for annotations using this link).
As an example, the following code snippet from the Polyspace Code Prover Demo shows an Out Of Bound Array Index proven unsafe check (OBAI). I have added an annotation (with the new syntax) to indicate that I plan to fix the OBAI later.
 static char reset_temperature(u8 in_v3)
 {
    int array[255-(54 * BIN_v3)];
    /* polyspace RTE:OBAI [To fix:High] "Enter a comment" */
    array[in_v3-255] = 0;
    return array[in_v3-255];
 }
When relaunching the analysis with Polyspace Code Prover 2017b or later, my annotation is not taken into account.

Best Answer

With the old annotation syntax prior to R2017b, you had to put your annotations on the line before the finding you wanted to annotate.
 /* polyspace<RTE:OBAI:High:To fix>  Enter a comment */
 array[in_v3-255] = 0;
With the new annotation syntax your annotation must be on the same line as the finding. This placement is more intuitive and adding annotations does not affect the number of lines in your source code. If you want your annotation to apply to multiple lines, you must specify that explicitly (Please read documentation in details).
So coming back to the previous example, you have to put the annotation on the same line as the finding, or keep it on the line before and add “+1” after the polyspace keyword:
 * /* polyspace +1 RTE:OBAI [To fix:High] "Enter a comment" */
   array[in_v3-255] = 0;
 * array[in_v3-255] = 0; /* polyspace RTE:OBAI [To fix:High] "Enter a comment" */
*Note: *Polyspace R2017b or later still supports code annotations that use the old syntax.
Related Question