クラス (-class-analyzer)

検証するクラスの指定

説明

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

Polyspace® が main の生成に使用するクラスを指定します。

オプションの設定

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

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

  • Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [実行時エラー] ノードを選択してから、このオプションを選択します。最初に有効にしなければならない他のオプションについては、依存関係を参照してください。

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

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

モジュールまたはライブラリを検証している場合、main 関数が存在しないと、Code Prover によって生成されます。main 関数が存在する場合、解析では既存の main が使用されます。

このオプションとオプション [指定クラス内で呼び出す関数] (-class-analyzer-calls) を使用して、生成された main が呼び出さなければならないクラス メソッドを指定します。main から直接または間接的に呼び出される場合を除いて、本ソフトウェアはそのクラス メソッドを解析しません。

設定

既定値: all

all

main 関数を生成するため、Polyspace はヘッダー ファイル外で 1 つ以上のメソッドが定義されているクラスをすべて使用します。生成された main は、オプション [指定クラス内で呼び出す関数] (-class-analyzer-calls) を使用して指定されたメソッドを呼び出します。

none

生成された main はどのクラス メソッドも呼び出せません。

custom

main 関数を生成するため、Polyspace は指定されるクラスを使用します。生成された main は、オプション [指定クラス内で呼び出す関数] を使用して指定されるクラスからメソッドを呼び出します。

依存関係

このオプションは、以下のすべてに該当する場合にのみ使用できます。

コードに main 関数が含まれている場合、このオプションは無視されます。

ヒント

  • このオプションで [none] を選択した場合、コード中で明示的に呼び出されないクラス メソッドは Polyspace では検証されません。

  • Polyspace は、インスタンス化されていないテンプレートを検証しません。クラス テンプレートを検証するには、テンプレートを使用してクラスを明示的にインスタンス化します。テンプレート クラス (Polyspace Code Prover)を参照してください。

コマンド ライン情報

パラメーター: -class-analyzer
値: all | none | custom=class1[,class2,...]
既定値: all
例 (Code Prover): polyspace-code-prover -sources file_name -main-generator -class-analyzer custom=myClass1,myClass2
例 (Code Prover Server): polyspace-code-prover-server -sources file_name -main-generator -class-analyzer custom=myClass1,myClass2

参考

| | |

トピック