MISRA C:2023 Dir 4.15

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

R2024a 以降

このページをすべて展開する

説明

このチェッカーは、既定の Polyspace® as You Code 解析では非アクティブにされます。Polyspace as You Code 解析で非アクティブにされるチェッカー (Polyspace Access)を参照してください。

命令の定義

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

根拠

浮動小数点式での算術または数学演算では、無限大や NaN (非数) が生成される可能性があります。無限大と NaN は特定のコンテキストで有用な特殊な表現ですが、検出されなければ、エラーや予期しない結果の原因となることがあります。無限大と NaN を想定していない関数には伝播することができないように、無限大と NaN を検出して処理します。

Polyspace 実装

Polyspace は以下の場合に違反を報告します。

  1. コード内で、浮動小数点値が、数学演算または関数呼び出しなどによって計算される。

  2. 計算された浮動小数点値が、別の関数に値渡しされるものの、その値が無限大や NaN であるかどうかがチェックされない。

計算された浮動小数点値が比較演算で使用される場合、またはグローバル変数に代入される場合には、Polyspace は違反を報告しません。

違反を回避するには、関数 isfinite() を使用して値が有限であるかどうかをチェックします。isnan() と isinf() を組み合わせて使用して、無限大の浮動小数点値をチェックした場合、Polyspace は違反を報告します。

このルール チェッカーが違反を報告するのは、オプション [非有限の浮動小数点を検討] (-allow-non-finite-floats) を指定した場合のみです。このオプションを指定すると、複数の欠陥チェッカーとコーディング ルール チェッカーが無効になります。

トラブルシューティング

ルール違反を想定していてもその違反が表示されない場合、コーディング規約違反が想定どおりに表示されない理由の診断を参照します。

例

すべて展開する

この例では、関数 produce_results() が無限大または NaN である可能性のある浮動小数点値を返します。produce_restults() から返される値が無限大および NaN であるかをチェックせずに、関数 consume_result() がその値を使用する場合、ルール チェッカーは違反を報告します。

#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 */
	}
}

この例を実行するには、オプション [非有限の浮動小数点を検討] (-allow-non-finite-floats) を有効にします。

チェック情報

グループ: Code design
カテゴリ: 必要
AGC カテゴリ: 必要

バージョン履歴

R2024a で導入

参考

トピック

1 All MISRA coding rules and directives are © Copyright The MISRA Consortium Limited 2021.

The MISRA coding standards referenced in the Polyspace Bug Finder™ documentation are from the following MISRA standards:

  • MISRA C:2004

  • MISRA C:2012

  • MISRA C:2023

  • MISRA C++:2008

  • MISRA C++:2023

MISRA and MISRA C are registered trademarks of The MISRA Consortium Limited 2021.