解析精度の構成

Code Prover の仮定と検証精度を構成する

精度オプションを使用して、検証の精度を構成します。検証の精度を高めると、オレンジチェックの数は減少しますが、より多くの計算リソースが必要になります。以下を構成できます。

グローバル精度 — エンジンレベルで精度に影響するオプションを指定します。これらの精度オプションは、あらゆる Polyspace^® Code Prover™ 解析に影響する可能性があります。
ファイルおよび関数 — これらのオプションは、Code Prover による関数とソースファイルの解析方法を指定します。
配列およびポインター — これらのオプションは、配列とポインターのモデル化および解析方法を指定します。
アセンブリコード — これらのオプションは、アセンブリ関数の処理方法を指定します。

Polyspace オプション

`状況依存性 (-context-sensitivity)`	エラーの原因となった関数呼び出しを識別する呼び出しコンテキスト情報の保存
`手続き間解析の精度を高める (-path-sensitivity-delta)`	行数が少ないコードに対する特定の検証の近似の回避
`特定の精度 (-modules-precision)`	残りの検証よりも高い精度で検証するソースファイルの指定

`-consider-external-array-access-unsafe`	サイズの指定されていない外部配列に任意のインデックスで安全にアクセスできるという既定の仮定の削除
`-improve-pointer-analysis-precision`	Enable more precise pointer analysis mode in Code Prover (R2022a 以降)
`-no-assumption-on-absolute-addresses`	絶対アドレスの使用が有効であるという仮定の削除
`環境ポインターが安全でないことを考慮する (-stubbed-pointers-are-unsafe)`	制約を設けない限り、環境ポインターはデリファレンスに対して安全でない可能性があることを指定
`-consider-external-array-access-unsafe`	サイズの指定されていない外部配列に任意のインデックスで安全にアクセスできるという既定の仮定の削除
`-improve-pointer-analysis-precision`	Enable more precise pointer analysis mode in Code Prover (R2022a 以降)

`-asm-begin -asm-end`	コンパイラ固有の `asm` 関数の解析からの除外
`アセンブリコードを無視 (-ignore-assembly-code)`	Specify that assembly instructions in C/C++ code cannot modify C/C++ variables (R2023a 以降)
`アセンブリコードを無視 (-ignore-assembly-code)`	Specify that assembly instructions in C/C++ code cannot modify C/C++ variables (R2023a 以降)

-code-behavior-specifications コードの要素 (関数など) への動作の関連付け

浮動小数点の丸めモード (-float-rounding-mode) 浮動小数点演算の結果を判定する際に考慮する丸めモードの指定

フィールドに volatile 修飾子があることを考慮する (-consider-volatile-qualifier-on-fields) コード内のどの位置にあっても、構造体の volatile 修飾子付きフィールドは取り得るすべての値を含む可能性があると仮定