このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。
検証の前提条件
ソース コードに関するソフトウェア前提の設定
特定のコードの構成要素についてのグローバルな前提条件を指定するには、検証の前提条件オプションを使用します。たとえば、"すべての" 構造体フィールドで 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 以降) |
トピック
- Polyspace 解析オプションの指定
Polyspace® ユーザー インターフェイス、他の IDE、またはスクリプトで Polyspace 解析オプションを設定する。