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

ファイルごとの検証で各ソース ファイルにインクルードするファイルの指定

説明

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

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

ファイルごとの検証では、各ソース ファイル検証にインクルードするファイルを指定します。これらのファイルはコンパイルされた後、各検証にリンクされます。

オプションの設定

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

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

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

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

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

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

ファイルごとの検証を行う場合、一部のファイルでは他のファイルに存在する情報が不足する場合があります。共通ファイルに不足している情報を配置し、このオプションを使用して、そのファイルを検証に指定します。たとえば、複数のソース ファイルが同じ関数を呼び出す場合、このオプションを使用してその関数定義または関数スタブを含むファイルを指定します。そうでない場合、Polyspace では、呼び出されてもソース ファイルで定義されていない関数に独自のスタブが使用されます。Polyspace のスタブに対する仮定は想定以上に広範囲に及び、オレンジ チェックにつながる可能性があります。

設定

既定値なし

をクリックしてフィールドを追加します。ファイルの絶対パスを入力します。あるいは、 ボタンを使用して、ファイルの場所に移動します。

依存関係

このオプションは、ファイルを個別に検証 (-unit-by-unit)を選択した場合にのみ有効にします。

コマンド ライン情報

パラメーター: -unit-by-unit-common-source
値: file1[,file2[,...]]
既定値なし
例 (Code Prover): polyspace-code-prover -sources file_name -unit-by-unit -unit-by-unit-common-source definitions.c
例 (Code Prover Server): polyspace-code-prover-server -sources file_name -unit-by-unit -unit-by-unit-common-source definitions.c

参考

(Polyspace Code Prover)

トピック