精度レベル (`-O0 | -O1 | -O2 | -O3`)

検証の精度レベルの指定

説明

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

検証で使用しなければならない精度レベルを指定します。

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

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

精度を高めると証明済み結果の数は増えますが、必要な検証時間も増加します。各精度レベルは、検証に使用されるアルゴリズムごとに対応します。

ほとんどの場合、精度と検証時間との最適なバランスはレベル 2 です。

既定値: 2

2: このオプションは、領域値の複雑な多面体モデルに対応していて、オプション [手続き間解析の精度を高める] (-path-sensitivity-delta) に応じて手続き間解析の精度をさらに高めます。

3: このオプションは、1000 行未満のコードにのみ適しています。このオプションを使用すると、証明される結果の割合が非常に高くなる可能性があります。

妥当な時間内に最良の結果を得るには、既定のレベル 2 を使用します。検証に長い時間がかかる場合は、精度を下げます。しかし、未証明のチェックの数が増加することがあります。同様に、オレンジチェックの数を減らすには精度を改善します。しかし、検証にかかる時間が大幅に長くなる可能性があります。
精度レベルが 2 以下のとき、その設定が有効になるのは、検証レベルが [Software Safety Analysis level 0] よりも高い場合のみとなります。検証レベル (-to) も参照してください。
たとえば、解析時間を短縮するには、検証レベルを [Software Safety Analysis level 0] に下げるという手段があります。解析時間をさらに短縮しようとして、精度レベルを 2 よりも下げてはいけません。
精度レベル 3 で使用されるアルゴリズムは、検証レベル [Software Safety Analysis level 0] にも適用可能であることに注意してください。

パラメーター: -O0 | -O1 | -O2 | -O3

既定値: -O2

例 (Code Prover): polyspace-code-prover -sources file_name -O1

例 (Code Prover Server): polyspace-code-prover-server -sources file_name -O1