Annotate Code for Justifying Polyspace Checks

Open Script

This example shows how Embedded Coder® uses operator annotations in the generated code to justify specific arithmetic operations and suppress Polyspace findings during static code analysis.

With Polyspace Code Prover™, you can perform Polyspace static verification on code generated by Embedded Coder. Polyspace detects run-time errors in the generated code and helps you identify modeling defects. In some cases, Polyspace reports overflows for operations that are safe by design because of how the code generator implements them. These findings should not be reported as errors. When you enable Operator annotations, Embedded Coder inserts comments in the generated code that document the intent of such operations. Polyspace uses these annotations to suppress the corresponding analysis results. The annotations are used only for analysis and do not affect the semantics of the generated C code. For more information, see Automated Justification of Coding Rule Violations (Polyspace Bug Finder).

Saturation Overflow Justification

This section shows how operator annotations justify saturation behavior in the generated code.

1. Open the example model mSatAddSub.

model='mSatAddSub';
open_system(model);

2. In the Embedded Coder app, open the Configuration Parameters dialog box and set Operator annotations to off.

set_param('mSatAddSub','OperatorAnnotations','off');

3. Build the model and generate code.

evalc('slbuild(''mSatAddSub'')');

Examine the generated code file:

file = fullfile('mSatAddSub_ert_rtw','mSatAddSub.c');
coder.example.extractLines(file,'/* Model step function */',...
    'USub = qY;');

/* Model step function */
void mSatAddSub_step(void)
{
  uint32_T qY;

  /* Sum: '<Root>/SubUnsigned' incorporates:
   *  Inport: '<Root>/In1'
   *  Inport: '<Root>/In2'
   */
  qY = U1 - U2;
  if (qY > U1) {
    qY = 0U;
  }

  /* Sum: '<Root>/SubUnsigned' */

The code generator performs the subtraction using the largest built-in integer type (32-bit) for U1 and U2. Because it is not possible to represent all saturated results directly, the generated code first performs the subtraction, then detects overflow, and finally applies explicit saturation logic. Polyspace may flag the subtraction as an arithmetic overflow because it does not infer the saturation logic, even though the final behavior is safe by design.

5. Enable Operator annotations on the Configuration Parameters dialog box and build the model.

set_param('mSatAddSub','OperatorAnnotations',"on");
evalc('slbuild(''mSatAddSub'')');

6. Examine the generated code:

file = fullfile('mSatAddSub_ert_rtw','mSatAddSub.c');
coder.example.extractLines(file,'/* Model step function */',...
    'USub = qY;');

/* Model step function */
void mSatAddSub_step(void)
{
  uint32_T qY;

  /* Sum: '<Root>/SubUnsigned' incorporates:
   *  Inport: '<Root>/In1'
   *  Inport: '<Root>/In2'
   */
  qY = U1 -
    /*MW:operator MISRA2012:D4.1 CERT-C:INT30-C 'Justifying MISRA C rule violation'*/
    /*MW:OvSatOk*/ U2;
  if (qY > U1) {
    qY = 0U;
  }

  /* Sum: '<Root>/SubUnsigned' */

When Operator annotations configuration parameter is enabled, Embedded coder inserts the /*MW:OvSatOk*/ comment. This annotation indicates that the arithmetic overflow is intentional and Polyspace uses this annotation to suppress the overflow error in its code analysis.

7. Close the model.

bdclose(model)

Justifying Carry or Borrow Detection (MW:OvCarryOk)

In some cases, the generated code intentionally relies on unsigned wraparound behavior to detect a carry or borrow condition. Polyspace may flag such operations as arithmetic overflows because it does not recognize that the wraparound behavior is intentional.

With Operator annotations enabled, Embedded Coder inserts the MW:OvCarryOk annotation to indicate that the operation is intentional.

uint32_T qY;
boolean_T borrow;

qY = U1 - /*MW:OvCarryOk*/ U2;
borrow = (qY > U1);

The MW:OvCarryOk annotation indicates that the overflow behavior is intentional and used to detect a carry or borrow condition. Polyspace suppresses the corresponding overflow analysis result.

Justifying Bitwise Truncation (MW:OvBitwiseOk)

In few cases, the generated code intentionally discards higher-order bits through bitwise operations such as masking. Polyspace may flag the arithmetic operation as an overflow because it does not recognize that the truncation is intentional.

With Operator annotations enabled, Embedded Coder inserts the MW:OvBitwiseOk annotation to indicate this behavior.

uint32_T qY;

qY = (U1 + /*MW:OvBitwiseOk*/ U2) & 0xFFU;

The MW:OvBitwiseOk annotation indicates that any overflow or bit loss caused by the operation is intentional due to subsequent bitwise processing. Polyspace suppresses the corresponding analysis results.

See Also

Topics