Annotating Single Line of Code

To annotate a result on the current line of code (including macros), use this syntax:

line of code; /* polyspace Family:Result_name */

For instance:

var++; /* polyspace DEFECT:INT_OVFL */

Annotations begin with the keyword polyspace and must include the Family and Result_name field values.

You can optionally specify a Status, Severity, and Comment field value:

polyspace Family:Result_name [Status:Severity] "Comment"

For instance:

var++; /* polyspace DEFECT:INT_OVFL [Justified:Low] "Overflow taken into account."*/

If you do not specify a status, Polyspace considers the result justified, and assigns the status No action planned to the result.

For further details, see Annotation Syntax Details and Syntax Examples.

Annotating Code Block

To annotate a block of code, use the following syntax. Note that the annotations apply only to the block of code itself and not to bodies of functions called from the block.

Optionally, specify a status, severity and comment.

If annotations for results with the same Family and Result_name are nested, the innermost annotation is used.

For example, in this code, the annotation on line 9 is applied instead of the block annotation, but the block annotation is applied to the violation on line 7.

1  /*polyspace-begin MISRA-C:14.9 [To fix:High] */
2  int main(void) 
3  {
4      int x = 1;
5      int y = x / 2;
6  
7      if (y < 0) /* Block annotation is applied to this violation of MISRA-C:14.9*/
8          y++;
9      if (x > y) /*polyspace MISRA-C:14.9 [Justified:Low] */
10         return x;
11     return x;
12 }
13 /*polyspace-end MISRA-C:14.9 [To fix:High] "Block annotation"*/

If you apply an annotation to multiple lines of code, the annotation does not apply to green checks in the code. When you rerun the analysis these green checks are not considered justified, and their Status and Severity in the Results List do not change to the Status and Severity of the annotation.

When you annotate a code block, the annotation applies only to the issues that arise from within the block. For instance, say you have a function call in the annotated block, and the body of the function gives rise to a violation. This violation is not affected by the annotation around the code block where the function is called.

For further details, see Annotation Syntax Details and Syntax Examples.

Justifying Multiple Results in the Same Line of Code

If a line of code contains more than one result, you can justify the results by using this syntax:

Optionally, specify a status, severity and comment.

For further details, see Annotation Syntax Details and Syntax Examples.

/* polyspace Family_1:Result_1_name "comment 1" polyspace Family_2:Result_2_name "comment 2"*/

Annotation Syntax Details

To replace the different annotation fields with their allowed values, use the values in this table or see the examples.

Suppress a Single Defect

Enter an annotation on the same line as the defect and specify the Family (DEFECT) and the Result_name (INT_OVFL). When you do not specify a status, Polyspace assigns the status No action planned, and then suppresses the result in subsequent analyses.

int var = INT_MAX;
var++; /* polyspace DEFECT:INT_OVFL */

Suppress a Single Coding Standard Violation

Justify a coding standard violation, for instance, a CERT-C violation.

Enter an annotation on the same line as the violation and specify the Family (CERT-C) and the Result_name (the rule number, for instance, STR31-C). Assign the status Justified, severity Low and a comment.

line of code; /* polyspace CERT-C:STR31-C [Justified:Low] "Overflow cannot happen
                                            because of external constraints." */

Suppress All MISRA C: 2012 Violations Over Multiple Lines

Enter an annotation with +n between polyspace and the Family:Result_name entries. The annotation applies to the same line and the n following lines.

This annotation applies to lines 4–7. The line count includes code, comments, and blank lines.

4. line of code ; // polyspace +3 MISRA2012:* 
5. //comment
6. 
7. line of code;
8. line of code;

Suppress All Code Metrics on Function

To annotate function-level code complexity metrics, in the function definition, enter an annotation on the same line as the function name.

This annotation suppresses all code complexity metrics for function func:

char func(char param) { //polyspace CODE-METRICS:*
   ...
}

Specify Multiple Families in the Same Annotation

Enter each family separated by a space. This annotation applies to all MISRA C:2012 rules 17 and to all run-time checks.

line of code; /* polyspace MISRA2012:17.* RTE:* */

Specify Multiple Result Names in the Same Annotation

After you specify the Family (DEFECT), enter each Result_name separated by a comma.

system("rm ~/.config"); /* polyspace DEFECT:UNSAFE_SYSTEM_CALL,RETURN_NOT_CHECKED */

Suppress Result Showing Global Variable Usage

To justify a Code Prover result showing global variable usage, for instance, an unused global variable, enter the annotation next to the variable declaration.

For instance, to suppress a global variable result with a Justified status, Low severity and some comments, you can enter an annotation like this:

int var; /* polyspace VARIABLE:* [Justified: Low] "Storage repo for later use"*/

Add Explanatory Comments to Annotation

After you specify a Family and a Result_name, you can add a Comment with additional information for your justification. You can provide a comment for all families and result names, or a comment for each family or result name.

Set Status and Severity

You can specify allowed values or enter custom values for status and severity. A custom severity entry is appended to the status and stored as a custom Status in the user interface.

//Set Status only
line of code; /* polyspace DEFECT:* [To fix] "some comment" */

//Set Status 'To fix' and Severity 'High'
line of code; /* polyspace VARIABLE:* [To fix: High] "some comment"*/

//Set custom status 'Assigned' and Severity 'Medium'
line of code; /* polyspace MISRA2012:12.* [Assigned: Medium] */

Justify Violations in a Code Block

Use annotation to justify violations arising from a block of code. For instance, consider this code:

double foo(void){
	constexpr int speedLimit = 65;
	constexpr double coeff = 0.2;
	int flag{0};
	int negOne{-1};
	//... 
	return (flag)?speedLimit*coeff*negOne
	: speedLimit*coeff*negOne - 35; //Noncompliant
}

int main(){
	
	/* polyspace-begin AUTOSAR-CPP14:A5-1-1 [Justified: Low]"Known Constant"*/
	//....
	for(int i = 0; i<10;++i){
		foo();
		//...
	}
	
	/* polyspace-end AUTOSAR-CPP14:A5-1-1  [Justified: Low]"Known Constant"*/
	return 1;
}

The annotated block contains a call to the function foo(). The annotations do not apply to the body of this function. For instance, the violation in the return statement of foo() appears as an unreviewed defect.

Annotate Results in Spliced Lines

Annotate results that appear in a spliced line of code. Consider this code:

#include <stdio.h>

#define NULL_PTR ((void*)0)

extern  int *value; 
extern int *ptr[10];
void callfoo(int **);

void t1(int val) {
  callfoo(&value);
    /* polyspace +1 RTE:OVFL */
    printf("Dereferenced value: %d %d %d %d\n", NULL_PTR, *ptr[val], *value+val, \
  val);
}