Main Content

MISRA C:2012 Dir 4.15

Evaluation of floating-point expressions shall not lead to the undetected generation of infinities and NaNs

Since R2024a

Description

This checker is deactivated in a default Polyspace® as You Code analysis. See Checkers Deactivated in Polyspace as You Code Analysis (Polyspace Access).

Directive Definition

Evaluation of floating-point expressions shall not lead to the undetected generation of infinities and NaNs.

This rule comes from MISRA C™: 2012 Amendment 3.

Rationale

Arithmetic or mathematical operations on floating-point expressions can lead to infinities and NaNs (not-a-number). Infinities and NaNs are special representations that are useful in specific contexts but can lead to errors or unexpected results if they are undetected. Detect and handle infinities and NaNs so that they cannot propagate to functions that do not expect them.

Polyspace Implementation

Polyspace reports a violation when:

  1. A floating-point value is computed in your code, for example, by a mathematical operation or by a function call.

  2. The computed floating-point value is then passed by value to another function but the value is not checked for infinities and NaNs.

Polyspace does not report a violation if the computed floating-point value is used in a comparison operation or assigned to a global variable.

To avoid a violation, use the function isfinite() to check if a value is finite. If you use a combination of isnan() and isinf() to check for nonfinite floating-point values, Polyspace reports a violation.

This rule checker reports violation only if you specify the option Consider non finite floats (-allow-non-finite-floats). Specifying this option disables several defect checkers and coding rule checkers.

Troubleshooting

If you expect a rule violation but do not see it, refer to Diagnose Why Coding Standard Violations Do Not Appear as Expected.

Examples

expand all

In this example, the function produce_results() returns a floating-point value that can be infinite or NaN. The rule checker reports a violation when the function consume_result() uses the value returned by produce_restults() without checking for infinity and NaN.

#include <math.h>
double produce_result(void);
void consume_result(double);

void foo(void) {
	double x = produce_result();
	// Use of x without checking for infinity and NaN
	consume_result(x);      /* Noncompliant */

	// x can be infinite
	if(!isnan(x)) {
		consume_result(x);  /* Noncompliant */
	}

	// x can be NaN
	if(!isinf(x)) {
		consume_result(x);  /* Noncompliant */
	}

	//Use x only if it is finite
	if(isfinite(x)) {
		consume_result(x);  /* Compliant */
	}
}

To run this example, enable the option Consider non finite floats (-allow-non-finite-floats).

Check Information

Group: Code design
Category: Required
AGC Category: Required

Version History

Introduced in R2024a