メインコンテンツ

構造体内の検証の深さの設定

構造体内の検証の深さを設定することを指定する

R2023b 以降

説明

この名前のオプションは、Polyspace Platform (Polyspace Test) ユーザー インターフェイスでのみ利用可能です。標準の Polyspace® ユーザー インターフェイスにおける同等のオプションについては、構造体内の検証の深さ (-k-limiting) を参照してください。

オプション [構造体内の検証の深さ] (-k-limiting) を設定するかどうかを指定します。

オプションの設定

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

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

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

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

コードが多数のレベルで構造化されていると、Polyspace Code Prover™ 検証に想定より時間がかかる場合があります。そのような場合は、このオプションを使用して、オプション [構造体内の検証の深さ] (-k-limiting) を有効にし、検証の深さを制限できるようにします。

設定

オン

Polyspace はオプション [構造体内の検証の深さ] (-k-limiting) を有効にします。

オフ (既定の設定)

Polyspace は [構造体内の検証の深さ] (-k-limiting) フィールドを無効のままにします。

コマンド ライン情報

パラメーター: -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

バージョン履歴

R2023b で導入