標準ライブラリの数学関数での Polyspace の過大近似の修正

問題

検証結果で、標準ライブラリの数学関数が想定どおりに動作しません。

たとえば、ステートメント assert(isinf(x)) で後続のステートメントの x の値が正または負の無限大に制約されません。

原因

Polyspace^® で数学関数の定義が見つからない場合、標準ライブラリの数学関数の Polyspace 実装が検証で使用されます。

場合によっては、関数の Polyspace 実装が関数の仕様と一致しないことがあります。そのような場合、Polyspace 実装では関数の動作の過大近似が行われます。たとえば、ステートメント assert(isinf(x)) に続く x の値の範囲に正と負の無限大が含まれる場合などがあります。したがって、そのような動作はグリーンチェックにならず、ランタイムエラーの原因となる可能性がある演算と見なされます。

解決法

コンパイラの関数の実装を検証で使用するように、コンパイラのネイティブのヘッダーファイルのパスを明示的に指定します。たとえば、一部のコンパイラでは、isinf などの関数をマクロとしてヘッダーファイルで実装します。

コマンドラインから検証を実行している場合は、オプション-Iを使用します。
ユーザーインターフェイスから検証を実行している場合は、ユーザーインターフェイスでの Polyspace の実行を参照してください。

クロスコンパイラを使用してビルドシステムから Polyspace プロジェクトを作成した場合、そのプロジェクトではコンパイラから提供されたヘッダーファイルが使用されます。