構造体内の検証の深さ (`-k-limiting`)

入れ子構造体の解析の深さの制限

説明

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

入れ子構造体の解析の深さに対する制限を指定します。

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

Polyspace^® ユーザーインターフェイス (デスクトップ製品のみ): プロジェクト構成で [スケーリング] ノードを選択してから、このオプションの値を選択します。
Polyspace Platform ユーザーインターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [実行時エラー] 、 [スケーリング] ノードを選択してから、このオプションの値を入力します。最初に有効にしなければならない他のオプションについては、依存関係を参照してください。
コマンドラインとオプションファイル: オプション -k-limiting を使用します。コマンドライン情報を参照してください。

多くのレベルの深さがある構造体がコードに含まれているため解析時間がかかる場合は、このオプションを使用します。

通常、階層の深い構造体によって検証時間が長くなると、警告メッセージが表示されます。

このオプションを使用するには、Polyspace Platform ユーザーインターフェイスでオプション [構造体内の検証の深さの設定] を "オン" () に設定する必要があります。

既定値: 入れ子構造体の最大の深さが解析されます。

入れ子構造体の解析の深さを指定する数値を入力します。たとえば 0 を指定した場合、この解析では構造体内の構造体は検証されません。

2 未満の数値を指定した場合、検証の精度が低くなる可能性があります。

パラメーター: -k-limiting

値: positive integer

例 (Code Prover): polyspace-code-prover -sources file_name -k-limiting 3

例 (Code Prover Server): polyspace-code-prover-server -sources file_name -k-limiting 3