ファイルを個別に検証 (`-unit-by-unit`)

各ソースファイルを他のソースファイルと別個に検証するオプション

説明

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

このオプションは、MATLAB^® コードまたは Simulink^® モデルから生成されたコードでは使用できません。

[ファイルを個別に検証] オプションにより、各ソースファイルを他のソースファイルとは別個に検証するかどうかを指定します。このオプションを有効にすると、Code Prover では各ファイルをモジュール内の他のファイルとは別個に検証します。プロジェクト全体または個々のファイルの検証結果を確認できます。

1 つのファイルの検証結果を開いた後、Polyspace^® デスクトップ製品のユーザーインターフェイスの [ダッシュボード] ペインですべてのファイルの結果の概要を確認できます。この概要テーブルから各ファイルの結果を直接開くことができます。

各結果ファイルは (ps_results.pscp という名前で) 結果フォルダーのサブフォルダーに保存されています。サブフォルダーの名前は、解析するソースファイルと同じ名前です。

Code Prover では、検証の開始点として main 関数が必要です。ファイルごとのモードでは、ほとんどのファイルに main 関数がないため、必要に応じて main 関数が Code Prover によって生成されます。既定では、生成された main 関数は、呼び出されていない関数 (C++ の呼び出されていない非プライベートメソッドやクラス外の関数) を呼び出します。詳細は、次を参照してください。

オプションの設定

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

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

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

さまざまな理由で、各ソースファイルを他のソースファイルとは別に検証することがあります。たとえば、プロジェクトの検証にかなりの時間がかかる場合は、ファイルごとの検証を実行して、検証に時間がかかっているファイルを特定します。

設定

オン: Polyspace は、各ソースファイルごとに別々の検証ジョブを作成します。
オフ (既定の設定): Polyspace は、モジュール内のすべてのソースファイルを対象に単一の検証ジョブを作成します。

依存関係

このオプションは、[モジュールまたはライブラリの検証] (-main-generator) を選択した場合にのみ有効になります。

ヒント

ファイルごとの検証を実行する場合、マルチタスキングオプションは指定できません。
プロジェクト全体の検証にかなりの時間がかかる場合は、ファイルごとの検証を実行します。ファイルの検証が完了後、他のファイルを検証中に結果を表示できます。
検証結果のレポートは、ファイルごとに生成することも、すべてのファイルをまとめて生成することもできます。すべてのファイルを対象として単一のレポートを生成するには、レポート生成を (解析オプションを使用して検証と同時に実行せずに) 検証後に実行します。
Polyspace ユーザーインターフェイスですべてのファイルを対象として単一のレポートを生成するには、次を行います (デスクトップ製品のみ)。
1. 1 つのファイルの結果を開きます。
2. [レポート作成] 、 [レポートの実行] を選択します。レポートを生成する前に、オプション [すべてのユニットの結果を含む単一のレポートを生成] を選択します。
Polyspace Platform ユーザーインターフェイスですべてのファイルを対象として単一のレポートを生成するには、次を行います (デスクトップ製品のみ)。
1. 1 つのファイルの結果を開きます。
2. [レポート] 、 [レポートの実行] を選択します。レポートを生成する前に、オプション [すべてのファイルのレポート] を選択します。
Polyspace Code Prover™ Server™ 製品を使用して検証を実行する場合、すべてのファイルを対象として単一のレポートを生成するには、次を行います。
- すべてのファイルの結果を Polyspace Access サーバーにアップロードします。
- オプション -all-units を指定した polyspace-report-generator コマンドを使用して、すべてのファイルを対象とした単一のレポートを生成します。
ファイルごとの検証を実行すると、使用されない変数のインスタンスが多数表示される可能性があります。これらの変数の一部は、他のファイルで使用されていても、ファイルごとの検証では未使用として表示される場合があります。
これらの結果を無視したい場合は、使用されていない変数をフィルターで除外するレビュースコープ (フィルターの名前付きセット) を使用します。Polyspace デスクトップユーザーインターフェイスでの結果のフィルター処理とグループ化を参照してください。

コマンドライン情報

パラメーター: -unit-by-unit

既定値: オフ

例 (Code Prover): polyspace-code-prover -sources file1,file2,... -unit-by-unit

例 (Code Prover Server): polyspace-code-prover-server -sources file1,file2,... -unit-by-unit

参考

共通のソースファイル (-unit-by-unit-common-source)

トピック

Polyspace 解析オプションの指定

ファイルを個別に検証 (-unit-by-unit)

説明