標準ライブラリの浮動小数点ルーチンの無効な使用

このトピックでは、Polyspace^® Code Prover™ の浮動小数点ルーチンに対する [標準ライブラリルーチンの無効な使用] チェックについて説明します。

Polyspace Code Prover では、標準ライブラリルーチンについて [標準ライブラリルーチンの無効な使用] チェックを実行し、その引数が有効かどうかを判定します。このチェックの動作は、メモリルーチン、浮動小数点ルーチン、文字列ルーチンのいずれが対象であるかによって異なります。ルーチンによって引数が無効になる状況が異なるためです。このトピックでは、標準ライブラリの浮動小数点ルーチンについてのチェックの仕組みを説明します。

チェックについての詳細は、標準ライブラリルーチンの無効な使用を参照してください。

チェックされる内容

[標準ライブラリルーチンの無効な使用] チェックでは、浮動小数点ルーチンの使用について次の問題がないかどうかを順番に調べます。

定義域エラー: 定義域エラーは関数の引数が無効な場合に発生します。無効な引数の定義は、非有限の浮動小数点を許可しているかどうかによって異なります。非有限の浮動小数点を許可している場合、次のようになります。
- NaN の結果について警告するように指定している場合は、関数が NaN を返し、引数自体は NaN でないと、定義域エラーが発生します。
- NaN の結果を禁止するように指定している場合は、関数が NaN を返すか、引数自体が NaN であると、定義域エラーが発生します。
詳細は、NaN (-check-nan)を参照してください。
このチェックの動作は浮動小数点での無効な演算のチェックとほぼ同じです。[標準ライブラリルーチンの無効な使用] チェックは標準ライブラリ関数に対して実行され、[浮動小数点での無効な演算] チェックは浮動小数点変数を含む数値演算に対して実行されます。
オーバーフローエラー: オーバーフローエラーは関数の結果がオーバーフローする場合に発生します。オーバーフローの定義は、非有限の浮動小数点を許可しているかどうかと指定した丸めモードによって異なります。非有限の浮動小数点を許可しており、無限大の結果について警告するように指定している場合は、関数が無限大を返し、引数自体は無限大でないと、オーバーフローエラーが発生します。詳細は、無限大 (-check-infinite)を参照してください。
このチェックの動作はオーバーフローのチェックと同じです。[標準ライブラリルーチンの無効な使用] チェックは標準ライブラリ関数に対して実行され、[オーバーフロー] チェックは浮動小数点変数を含む数値演算に対して実行されます。
無効なポインター引数: ポインター引数を受け取る frexp などの関数の場合、検証ではポインターのデリファレンスが有効かどうかがチェックされます。ポインターが NULL ではない、許容範囲外を指していないなどです。

このチェックでは、これらのエラーについて順番に確認されます。

チェックで明確な定義域エラーが見つかった場合は、オーバーフローエラーは確認されません。
チェックで可能性のある定義域エラーが見つかった場合は、定義域エラーが発生しない実行パスについてのみオーバーフローエラーが確認されます。

各エラーのチェック自体が複数の条件で構成され、それらについても順番にチェックされることがあります。各チェックは前のチェックにパスした実行パスについてのみ実行されます。

チェックされる単一引数の関数

[標準ライブラリルーチンの無効な使用] チェックでカバーされるルーチン、その単精度バージョン (接尾辞 f、ある場合) およびその long double バージョン (接尾辞 l) は次のとおりです。チェックは、C および C++ コードの場合とまったく同じように機能します。

acos
acosh
asin
asinh
atan
atanh
ceil
cos
cosh
exp
exp2
expm1
fabs
floor
log
log10
log1p
logb
round
sin
sinh
sqrt
tan
tanh
trunc
cbrt

引数が複数の関数

atan2
fdim
fma
fmax
fmin
fmod
frexp
hypot
ilogb
ldexp
modf
nextafter
nexttoward
pow
remainder

参考

非有限の浮動小数点を検討 (-allow-non-finite-floats) | 浮動小数点の丸めモード (-float-rounding-mode)