このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

検証の前提条件

ソース コードに関するソフトウェア前提の設定

特定のコードの構成要素についてのグローバルな前提条件を指定するには、検証の前提条件オプションを使用します。たとえば、"すべての" 構造体フィールドで NULL または volatile 修飾子となる可能性がある "すべての" 外部ポインターを考慮しなければならないことを指定します。特定の変数、関数、またはファイルに適用するローカルな前提条件については、入力およびスタブのオプションを使用します。

前提条件のより包括的なリストについては、Code Prover 解析の前提条件を参照してください。

Polyspace オプション

浮動小数点の丸めモード (-float-rounding-mode)浮動小数点演算の結果を判定する際に考慮する丸めモードの指定
環境ポインターが安全でないことを考慮する (-stubbed-pointers-are-unsafe)制約を設けない限り、環境ポインターはデリファレンスに対して安全でない可能性があることを指定
フィールドに volatile 修飾子があることを考慮する (-consider-volatile-qualifier-on-fields)コード内のどの位置にあっても、構造体の volatile 修飾子付きフィールドは取り得るすべての値を含む可能性があると仮定
アセンブリ コードを無視 (-ignore-assembly-code)Specify that assembly instructions in C/C++ code cannot modify C/C++ variables (R2023a 以降)

トピック