手続き間解析の精度を高める (`-path-sensitivity-delta`)

行数が少ないコードに対する特定の検証の近似の回避

説明

このオプションは Code Prover 解析のみに影響します。

少量のコードの場合、このオプションを使用して、関数間解析の精度を高めます。

以下のいずれかの方法を使用してオプションを設定します。

Polyspace^® ユーザーインターフェイス (デスクトップ製品のみ): プロジェクト構成で [精度] ノードを選択してから、このオプションの値を入力します。
Polyspace Platform ユーザーインターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [実行時エラー] 、 [精度] ノードを選択してから、このオプションの値を入力します。
コマンドラインとオプションファイル: オプション -path-sensitivity-delta を使用します。コマンドライン情報を参照してください。

このオプションは、実行パスでソフトウェアによる特定の近似を回避するために使用します。このような近似を回避することによりオレンジチェックは減らせますが、検証時間はずっと長くなります。

たとえば、関数呼び出しの階層構造が深い場合や条件付きステートメントが入れ子になっている場合、検証を妥当な時間で完了できるよう多数の実行パスが結合され、検証の各段階で保存される情報が減らされます。このオプションを使用する場合、実行パスについてより多くの情報が保存され、検証がより正確なものとなります。

既定値: オフ

このオプションをオンに設定するには正の整数を入力します。

入力する値を大きくすると証明される結果の数は増えますが、検証時間も指数関数的に増加します。たとえば、10 の値を入れると検証時間が非常に長くなる可能性があります。

このオプションはコードが 1000 行未満の場合にのみ使用してください。

パラメーター: -path-sensitivity-delta

値: 正の整数

例 (Code Prover): polyspace-code-prover -sources file_name -path-sensitivity-delta 1

例 (Code Prover Server): polyspace-code-prover-server -sources file_name -path-sensitivity-delta 1