検証レベル (-to)

コードに対する検証プロセスの実行回数の指定

説明

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

ソース コードに対する Polyspace^® 検証プロセスの実行回数を指定します。実行するたびに証明済み結果の数は増えますが、必要な検証時間も増加します。

オプションの設定

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

• Polyspace ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [精度] ノードを選択してから、このオプションの値を選択します。

• Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [実行時エラー] 、 [精度] ノードを選択してから、このオプションの値を選択します。

• コマンド ラインとオプション ファイル: オプション -to を使用します。コマンド ライン情報を参照してください。

このオプションを使用する理由

さまざまな理由で、検証レベルを上げたり下げたりする場合があります。たとえば、検証後に多くのオレンジ チェックが表示される場合は、検証レベルを上げてみます。解析に想定より長時間かかる場合は、検証レベルを下げてみます。

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

設定

既定値: Software Safety Analysis level 2

Source Compliance Checking

Polyspace はコンパイル エラーのみをチェックします。

Software Safety Analysis level 0

検証プロセスにおいて、いくつかの単純な解析を実行します。この解析は、コードが複雑であっても完了するように設計されています。

より高いレベルでの検証が停止してしまう場合は、このレベルで実行して結果を確認してください。

Software Safety Analysis level 1

検証プロセスにおいて、精度レベルに応じた複雑度をもつアルゴリズムで各関数を 1 度だけ解析します。精度レベル (-O) を参照してください。解析は、関数呼び出し階層 (実際の、または生成された main 関数) の一番上から開始され、その呼び出し階層の下層に伝播します。

Software Safety Analysis level 2

検証プロセスにおいて、各関数を 2 度解析します。1 回目の実行では、解析は関数呼び出し階層の一番上から下層に伝播します。2 回目の実行では、解析が下層から一番上に遡って伝播します。毎回の解析において、それまでの解析で収集した情報が使用されます。

最も正確な結果を妥当な時間内で得るには、このオプションを使用します。

Software Safety Analysis level 3

検証プロセスにおいて、各関数を 3 度解析します。解析は、関数呼び出し階層の一番上から下層に伝播し、下層から一番上に遡り、再度下層へと伝播します。毎回の解析において、それまでの解析で収集した情報が使用されます。

Software Safety Analysis level 4

検証プロセスにおいて、各関数を 4 度解析します。関数呼び出し階層の一番上から下層への解析を 2 度実行します。毎回の解析において、それまでの解析で収集した情報が使用されます。

other

このオプションを使用した場合、手動で停止しないかぎり Polyspace 検証は 20 回実行されます。

ヒント

• 検証に時間がかかりすぎる場合は、[検証レベル] を下げて使用してください。最適な結果を得るには、[Software Safety Analysis level 2] オプションを使用します。

• レッド エラーとグレー コードを訂正後、検証レベルを上げて検証を再度実行します。

• より低いレベルで最大精度の結果が得られた場合、検証は停止し、指定したレベルに進まないことがあります。高い検証レベルではメモリ不足で検証が失敗する場合でも、低いレベルの結果を利用可能であれば、Polyspace は低いレベルの結果を表示します。

• 検証時間が不当に長くなる可能性があるので、[Other] オプションは慎重に使用してください。

• Polyspace 解析をリモート サーバーで実行する場合、ソース フェーズはローカル コンピューターで実行されます。[検証レベル] を [Source Compliance Checking] に設定する場合は、-batch を使用してデスクトップからリモート サーバーにジョブを送信するということはしないでください。リモート クラスターで Bug Finder または Code Prover 解析を実行 (-batch) を参照してください。

• グローバル変数の共有と使用のみを表示するには、[グローバル変数の共有と使用のみを表示] (-shared-variables-mode) を使用して簡易解析を実行します。

コマンド ライン情報

パラメーター: -to

値: compile | pass0 | pass1 | pass2 | pass3 | pass4 | other

既定値: pass2

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

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

ユーザー インターフェイスでは使用できない以下の追加の値を使用することもできます。

• C プロジェクト:c-to-il (C から中間言語への変換段階)

• C++ プロジェクト:cpp-to-il (C++ から中間言語への変換段階)、cpp-normalize (C++ コンパイル)、cpp-link (C++ コンパイル)

明確な理由がある場合のみ、これらの値を使用します。たとえば、C++ プロジェクトで空白の制約 (DRS) テンプレートを生成するには、cpp-link または cpp-normalize を使用してコンパイルまでの解析を実行します。

値 cpp-link および cpp-normalize は将来のリリースで削除される予定です。代わりに compile を使用してください。

例

検証レベルを上げることでオレンジ チェックの数を減らす

検証レベルを上げて Code Prover 検証を実行すると、オレンジ チェッカーの数が減ります。

精度を [Software Safety Analysis level 0] に設定して、このコードに対して Code Prover 検証を実行します。

extern int tab[];

int main() {
    
    int i = tab[3];
    int j = tab[1];

    if (i > j) {
        int l = i-j;
        assert(l > 0);
     }
}

assert ステートメントにオレンジ チェックが表示されます。

このオレンジ チェックを解決するには、精度を上げて解析を実行します。たとえば、精度を [Software Safety Analysis level 1] に設定して、前のコードに対してもう一度検証を実行します。

extern int tab[];

int main() {
    
    int i = tab[3];
    int j = tab[1];

    if (i > j) {
        int l = i-j;
        assert(l > 0);
     }
}

今回は、assert ステートメントにグリーン チェックが表示されます。

参考

精度レベル (-O) | グローバル変数の共有と使用のみを表示 (-shared-variables-mode)

トピック

• Polyspace 解析オプションの指定
• 検証精度の向上