Annotate Source Code to Justify Known Missing Coverage

R2026b

Using Polyspace^® Test™, you can compute how much of your C/C++ code is covered by existing tests. Prior to coverage computation or based on reviewing previous coverage results, you can indicate locations in your source code where missing coverage is acceptable using source code annotations.

Polyspace coverage annotations let you explicitly mark code locations – for example, a function entry, a decision, or a specific condition outcome – as justified so that known and acceptable coverage gaps are excluded from coverage metrics and reports. You add the annotation as a C/C++ comment on the same line as the code construct that the gap refers to. The annotation contains a required [Justified] keyword and a free-form quoted reason.

Adding a source-code annotation to justify one or more missing coverage outcomes:

Shows the missing coverage outcomes as pre-justified in subsequent runs.
Prevents automatic test generation for these outcomes when you generate tests for missing coverage.

Annotation Syntax

You can add coverage annotations to a single line of code or multiple lines:

To apply a code coverage justification to a specific line of code, add a C/C++ comment with this syntax:
```
/* polyspace COV:<TYPE> [Justified] "reason" */
```
Use the coverage <TYPE> that best matches the coverage gap you want to justify. Place the annotation on the exact line that holds the construct (for example, on the line with if (...), the line with the switch keyword or the specific case label, the function signature, or the sub‑condition if you split compound decisions across lines).
To apply a code coverage justification to the next line of code, add a C/C++ comment with this syntax:
```
/* polyspace +1 COV:<TYPE> [Justified] "reason" */
```
You can generalize this syntax to apply to the next n lines of code:
```
/* polyspace +n COV:<TYPE> [Justified] "reason" */
```
To apply a code coverage justification to a block of code, include the block between C/C++ comments with this syntax:
```
/* polyspace-begin COV:<TYPE> [Justified] "reason" */

/* polyspace-end COV:<TYPE> [Justified] "reason" */
```

You can place more than one annotation on the same line if multiple gaps apply (for example, both an equality and a greater-than relational boundary are untested).

Follow these best practices when annotating source code for acceptable missing coverage:

Use outcome-specific annotations (for example, TRUE_DECISION_OUTCOME, FALSE_CONDITION_OUTCOME) when the decision/condition itself is executed but one outcome is never observed. Use the general form (for example, DECISION, CONDITION) when the construct is never exercised at all.
Keep the justification text concise and actionable (for example, “defensive fallback never triggered in production configuration”).

Annotations for Various Coverage Types

The following coverage types can be justified using code annotations. For each type, the corresponding canonical code form is shown:

* (wildcard) — Justify coverage results irrespective of coverage type.
```
/* polyspace COV:* [Justified] "reason" */
```
FUNCTION — Justify missing coverage for all coverage types within a function. Place this annotation on the same line as the function signature.
```
/* polyspace COV:FUNCTION [Justified] "reason" */
```
DECISION — Justify a decision that is never evaluated (entire if/switch not reached).
```
/* polyspace COV:DECISION [Justified] "reason" */
```
FALSE_DECISION_OUTCOME — Justify that the false branch of a decision is never taken (decision always true).
```
/* polyspace COV:FALSE_DECISION_OUTCOME [Justified] "reason" */
```
TRUE_DECISION_OUTCOME — Justify that the true branch of a decision is never taken (decision always false).
```
/* polyspace COV:TRUE_DECISION_OUTCOME [Justified] "reason" */
```
CONDITION — Justify a specific condition within a decision that is never evaluated at all.
```
/* polyspace COV:CONDITION [Justified] "reason" */
```
FALSE_CONDITION_OUTCOME — Justify that a condition is evaluated but its false outcome is never observed (condition always true).
```
/* polyspace COV:FALSE_CONDITION_OUTCOME [Justified] "reason" */
```
TRUE_CONDITION_OUTCOME — Justify that a condition is evaluated but its true outcome is never observed (condition always false).
```
/* polyspace COV:TRUE_CONDITION_OUTCOME [Justified] "reason" */
```
CASE_DECISION_OUTCOME — Justify an unexecuted switch case label.
```
/* polyspace COV:CASE_DECISION_OUTCOME [Justified] "reason" */
```
MCDC_OUTCOME — Justify a missing MC/DC objective (a condition not shown to independently affect the decision outcome).
```
/* polyspace COV:MCDC_OUTCOME [Justified] "reason" */
```
LESS_RELATIONAL_BOUNDARY_OUTCOME — Justify that a relational boundary region "less than" was never covered.
```
/* polyspace COV:LESS_RELATIONAL_BOUNDARY_OUTCOME [Justified] "reason" */
```
EQUAL_RELATIONAL_BOUNDARY_OUTCOME — Justify that the equality boundary (exactly on the threshold) was never covered.
```
/* polyspace COV:EQUAL_RELATIONAL_BOUNDARY_OUTCOME [Justified] "reason" */
```
GREATER_RELATIONAL_BOUNDARY_OUTCOME — Justify that a relational boundary region "greater than" was never covered.
```
/* polyspace COV:GREATER_RELATIONAL_BOUNDARY_OUTCOME [Justified] "reason" */
```
STATEMENT – Justify that a statement was not executed.
```
/* polyspace COV:STATEMENT [Justified] "reason" */
```
FUN_EXIT – Justify that a function exit point (return statement) was never reached.
```
/* polyspace COV:FUN_EXIT [Justified] "reason" */
```
FUN_CALL – Justify that a function call statement was not executed.
```
/* polyspace COV:FUN_CALL [Justified] "reason" */
```

Examples

These examples illustrate typical usage. Adjust the reason strings to match your project policy.

Justify an Entire Function for All Coverage Types

Annotate at the function entry to justify missing function coverage (and any derived metrics tied to the entry). Put the annotation on the same line as the function signature.

int legacy_handler(int code) { /* polyspace COV:FUNCTION [Justified] "Legacy path kept for backward compatibility; not exercised" */
    /* ... implementation ... */
    return -1;
}

Justify Missing Decision Coverage for a Decision

Annotate next to the branch point and use DECISION as coverage type when a decision (the whole if or switch) is never evaluated by your current tests.

if (mode == SAFE_MODE) /* polyspace COV:DECISION [Justified] "SAFE_MODE is disabled in this product variant" */
{
    engageFailsafe();
}

For a switch statement where none of the cases is reached, annotate next to the switch statement and use DECISION as coverage type:

switch (state) /* polyspace COV:DECISION [Justified] "State machine not active in product release" */
{
    case INIT:      
      init(); 
      break;
    case RUN:       
      run();  
      break;
    default:        
      idle(); 
      break;
}

Justify a Missing Decision Outcome

Annotate next to the branch point when a decision outcome is never evaluated by your current tests. Use TRUE_DECISION_OUTCOME or FALSE_DECISION_OUTCOME as coverage outcome type when the decision executes but one outcome never occurs.

/* Outcome always true: false branch never taken */
if (sensor_ok && armed) /* polyspace COV:FALSE_DECISION_OUTCOME [Justified] "armed is always true in certified builds" */
{
    launch();
}

/* Outcome always false: true branch never taken */
if (error_count > 100) /* polyspace COV:TRUE_DECISION_OUTCOME [Justified] "Counter capped below threshold by design" */
{
    reset();
}

For a switch statement where one of the cases in the switch expression is not reached, annotate next to the case or default and use CASE_DECISION_OUTCOME as coverage outcome type:


switch (state) 
{
    case INIT:
      init(); 
      break;
    case RUN:       
      run();  
      break;
    default: /* polyspace COV:CASE_DECISION_OUTCOME [Justified] "Idle state executed only for debug and test" */
      idle();
      break;
}

Justify Missing Condition Coverage

Annotate next to the branch point and use CONDITION as coverage type to justify an uncovered simple condition inside a decision, or the outcome-specific variants when only one side is untested.

/* Compound decision with one sub-condition never exercised */
if ((x < 0) && (y == 0)) /* polyspace COV:CONDITION [Justified] "y == 0 cannot occur with current configuration" */
{
    handle();
}

/* Outcome-specific justification for a condition that is executed but never false */
if ((speed >= limit) || emergency) /* polyspace COV:FALSE_CONDITION_OUTCOME [Justified] "emergency hardwired true on test bench" */
{
    clamp();
}

Justify Missing MC/DC Coverage

Annotate next to the branch point and use MCDC_OUTCOME as coverage outcome type when a specific condition within a compound decision has not been shown to independently affect the decision outcome (for example, you never toggled one condition while keeping the others fixed).

/* MC/DC: B and C not independently demonstrated */
if ((A || B) && C) /* polyspace COV:MCDC_OUTCOME [Justified] "B not independently toggled in this variant" */ /* polyspace COV:MCDC_OUTCOME [Justified] "C forced true for safety certification tests" */
{
    proceed();
}

Ignoring Code Annotations

To run a clean coverage analysis that ignores all code annotations, use the -ignore-code-annotations option with polyspace-code-profiler during instrumentation. Any /* polyspace COV:<TYPE> [Justified] ... */ annotations in your source code are not honored, and uncovered code that would otherwise be marked as justified is reported as not covered.

polyspace-code-profiler -instrument -instrum-dir instrumFolder -cov-metric-level mcdc -ignore-code-annotations -- gcc source.c

You cannot use this option together with -xml-annotations-description.

Alternative Annotation Syntaxes

If your codebase uses a third-party or custom annotation syntax to justify coverage results, use the -xml-annotations-description option with polyspace-code-profiler so that it recognizes those annotations. The option takes a path to an XML file that maps your alternative annotation syntax to the Polyspace annotation syntax.

polyspace-code-profiler -instrument -instrum-dir instrumFolder -cov-metric-level mcdc -xml-annotations-description annotations.xml -- gcc source.c

Without this option, custom annotations in your source code are not recognized and matching coverage results are not justified. With the option, annotations that match the patterns defined in the XML file justify the corresponding uncovered results. You cannot use this option together with -ignore-code-annotations.

For example, suppose your team uses a short inline comment format // COV_JUSTIFY: <reason> instead of the standard Polyspace annotation syntax:

SUM_STATUS resetIfOverflow(void) { // COV_JUSTIFY: Defensive function
    if (gSum == UINT_MAX) { // COV_JUSTIFY: Both branches tested at system level
        gSum = 0;
        return OVERFLOW_RESET;
    }
    return NOT_SATURATED;
}

To make Polyspace recognize these annotations, create an XML file that defines how to parse the comment and how to map it to a coverage result:

<?xml version="1.0" encoding="UTF-8"?>
<Annotations xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
             xsi:noNamespaceSchemaLocation="annotations_xml_schema.xsd"
             Group="custom coverage annotations">

  <Expressions Search_For_Keywords="COV_JUSTIFY"
               Separator_Result_Name="," >

    <Expression Mode="SAME_LINE"
                Regex="(COV_JUSTIFY):\s*(.*)"
                Rule_Identifier_Position="1"
                Default_Status="Justified"
                Comment_Position="2"
                />

  </Expressions>

  <Mapping>
    <Result_Name_Mapping Rule_Identifier="COV_JUSTIFY" Family="COV" Result_Name="*"/>
  </Mapping>
</Annotations>

The XML has two parts. The Expressions section tells Polyspace how to find and parse the annotation:

Search_For_Keywords — Only examine lines containing this keyword.
Regex — Match the annotation and define capture groups. Group 1 is the keyword itself, group 2 is the justification text after the colon.
Rule_Identifier_Position — Specifies which capture group is the rule identifier used to look up the mapping.
Comment_Position — Specifies which capture group is stored as the justification comment.
Default_Status — Matching annotations are treated as justified without requiring an explicit status token.
Mode — Controls the scope of justification. SAME_LINE applies only to results on the annotated line.

The Mapping section connects the parsed identifier to Polyspace results:

Rule_Identifier — Matches the value captured by the regex.
Family — The Polyspace result family to map to (COV for coverage).
Result_Name — The specific result type within the family. The wildcard * means all coverage types on that line are justified.

For the full annotation XML syntax, see the XSD schema at <polyspaceroot>\polyspace\verifier\annotation\annotations_xml_schema.xsd, where <polyspaceroot> is the Polyspace installation folder, for instance, C:\Program Files\Polyspace\R2026b.