Main Content

Address Polyspace Results by Annotating Simulink Blocks

When reviewing Polyspace® results, you might want to address known Polyspace results by adding justifications. Annotate the relevant Simulink® blocks with the justification in the Simulink Editor or the Polyspace User Interface. Polyspace supports annotating these results:

After you annotate a block, code operations generated from the block show results that are prepopulated with your comments. If you annotate a subsystem block or a block that leads to a function call, code operations generated from the block do not show your comments in the analysis results. If the block is a Lookup Table, enable the Stub lookup tables instead of using annotations. See Stub lookup tables.

In code generated by using Embedded Coder®, there are known deviations from MISRA C™:2012. See Deviations Rationale for MISRA C Compliance (Embedded Coder). Justify these known issues by annotating blocks.

Annotations in Simulink blocks or in generated code do not take the history of the analysis into account. If you update your model, the Polyspace results might change while the annotations do not. Updating the model might render the existing annotations outdated. Update your annotations when you update your model or generated code.

Annotate Blocks Through Polyspace User Interface

If you use Embedded Coder to generate code, you can annotate Simulink blocks directly through the Polyspace desktop user interface. Locate the issue that you want to annotate, and then enter review information by adding Severity, Status, and optional notes in the Result Details pane. For instance:

  • Set the Status of the issue to To Investigate

  • Set the Comment for the issue to Might Impact "Module"

In the source code, right-click the variable showing the issue (or another variable in the same expression) and from the context menu, select Annotate Block.

Right-click on a source code token that displays the result of a check and select the 'Annotate Block' option.

The review information carries over to the Simulink Editor as block annotation where the annotated block is highlighted.

An annotated block has the words 'Polyspace annotation' next to it.

You can annotate a Simulink block multiple times. Subsequent annotations on a block are appended to previous annotations. These annotations cannot be seen in the Simulink Editor. When you analyze the generated code by using Polyspace, these annotations are displayed as review information in the Result details pane of the Polyspace UI.

The option Annotate Block is available for code elements that can be traced to a Simulink block. For more information, see Trace Simulink Model Elements in Generated Code (Embedded Coder).

Annotate Blocks in Simulink Editor

To annotate a block in the Simulink Editor, select the block and on the Polyspace tab, select Add Annotation. In the Polyspace Annotation window:

  • Select the type of Polyspace result that you want to annotate from the drop-down list Annotation Type.

  • If you want to annotate multiple results of the same type, enter a comma-separated list of result acronyms in the text box. See:

  • If you want to annotate only one result, select Only 1 check. The text box is converted into a dropdown list. Select the result that you want to annotate from this dropdown list.

  • In the corresponding text boxes, enter the status, severity, and comment that you want to assign to the results.

The block shows the text Polyspace annotation. If the block has any preexisting Simulink annotations, they are preserved.

In the Polyspace Annotation window, you can annotate a single type of Polyspace result at a time. To annotate multiple types of results, open the Polyspace Annotation window multiple times. Each time, add an annotation corresponding to one type of Polyspace result. The different annotations are appended to each other. These annotations cannot be seen in the Simulink Editor. When you analyze the generated code by using Polyspace, these annotations are displayed as review information in the Result details pane of the Polyspace UI.

Sometimes operations in the generated code cause orange checks in Code Prover. Suppose an operation potentially overflows. The generated code protects against the overflow by following the operation with a saturation. Polyspace still flags the possible overflow as an orange check. To justify these checks through code comments, specify the configuration parameter Operator annotations (Embedded Coder).

Limitations

When you copy an annotated block, and then use it in a different model or in a different position in the same model, the changed context can render the annotation incorrect:

  • Polyspace does not allow annotation in blocks inside libraries and nonatomic subsystems because these blocks are reused in many different contexts. For instance, you cannot annotate a block inside a library block and justify results on all instances of the library block.

  • Simulink does not retain Polyspace annotations in blocks that are copied to a different model or in a different position in the same model.

Related Topics