このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。
polyspace-configure
(システム コマンド) DOS または UNIX コマンド ラインでビルド システムから Polyspace プロジェクトを作成
構文
説明
polyspace-configure システム コマンドは、ビルド コマンドから Polyspace® プロジェクトまたはオプション ファイルを作成します。
メモ
この Polyspace コマンドは polyspaceroot\polyspace\binpolyspacerootC:\Program Files\Polyspace\R2025a など) です (デスクトップ製品の場合はインストール フォルダー、サーバー製品の場合はインストール フォルダーも参照してください)。コマンドの絶対パスの入力を省略するには、この場所をオペレーティング システムの PATH 環境変数に追加します。
polyspace-configure  はビルド システムをトレースし、そのビルド システムから収集した情報によって Polyspace プロジェクトを作成します。Polyspace は、ビルド コマンドまたは makefile が一定の要件を満たしている場合にのみ、ビルド システムからプロジェクトを作成します。コンパイラおよびビルド コマンドの要件のリスト (Polyspace がサポートしているコンパイラのリストを含む) は、ビルド システムからのプロジェクト作成の要件を参照してください。buildCommand
polyspace-configure [ はビルド システムをトレースし、options] buildCommand options を使用して polyspace-configure の既定の動作を変更します。buildCommand の前に修飾子を指定します。指定しない場合、ビルド コマンド自体のオプションと見なされます。
polyspace-configure [ は、入力された JSON コンパイル データベース ファイル options] -compilation-database jsonFilejsonFile から収集された情報を使用して Polyspace プロジェクトを作成します。ビルド コマンドを指定したり、ビルド システムをトレースしたりする必要はありません。JSON コンパイル データベースの詳細については、JSON Compilation Database を参照してください。
例
入力引数
アルゴリズム
polyspace-configure コマンドは、おおまかに次の手順で make などのビルド コマンドから Polyspace プロジェクトまたはオプション ファイルを作成します。
- ビルド コマンドが最初に実行されます。 - polyspace-configureは、このビルドで実行されるコマンド、読み取られたファイル、書き込まれたファイルを追跡します。これらのコマンドの 1 つ以上がコンパイラを呼び出します。たとえば、ビルド コマンドが GCC コンパイラを使用する場合、これらのコマンドの 1 つ以上が- gcc、- g++、または関連する実行可能ファイルを実行します。既知のコンパイラ実行可能ファイルが存在しているかどうかに応じて、- polyspace-configureはビルド中に実行されたすべてのコマンドの中から、コンパイラ呼び出しコマンドを選択します。
- 各コンパイラ呼び出しコマンドは、3 つの部分 (コンパイラ実行可能ファイル、ソース ファイル、コンパイラ オプション) で構成されています。たとえば次のコマンドでは、C++11 ベースのコンパイルをトリガーするコンパイラ オプション - -stdで、ファイル- myFile.cに対して GCC コンパイラを実行します。- gcc -std=c++11 myFile.c - polyspace-configureはこれらのコマンドからソース ファイル名を読み取り、Polyspace プロジェクトまたはオプション ファイルで直接使用します。コンパイラ実行可能ファイルおよびコンパイラ オプションは、Polyspace 解析オプションに変換されます。- size_tの基本型または潜在型のサイズに対応するオプションなどの Polyspace オプションを判別するため、- polyspace-configureは以前に読み取られたコンパイラ実行可能ファイルとコンパイラ オプションを、いくつかの小さなソース ファイルに対して実行します。ソース ファイルのコンパイルが成功するか、またはエラーが表示されるかに応じて、- polyspace-configureは適切な Polyspace オプションを設定できます。コンパイラ マクロ定義とインクルード パスを判別するため、- polyspace-configureは小さなソースに対するコンパイラの再呼び出しも行いますが、それ以降は少し異なる手法を使用します。- Polyspace オプションの判別に役立つソース ファイルの簡単な例については、オプション - [size_t の管理] (-size-t-type-is)のリファレンス ページを参照してください。
ビルド コマンドの代わりに、polyspace-configure を使用して、JSON コンパイル データベースからプロジェクトまたはオプション ファイルを作成することもできます。polyspace-configure コマンドがコンパイル データベースで実行される場合、前述の最初のステップは省略されます。コンパイル データベースは、次のようなエントリでコンパイラ呼び出しコマンドを直接指定します。
{
"directory": "/proj/files/
"command": "/usr/local/bin/gcc -std=c++11 -c /proj/files/myFile.c",
"file" : "/proj/files/myFile.c"
}polyspace-configure は、これらのコンパイラ呼び出しコマンドを読み取り、小さなソース ファイルに対するコンパイラの再呼び出しの残りのステップを実行できます。ビルド コマンドの実行ステップが省略されるため、コンパイル データベースでの polyspace-configure の実行にかかる時間は、ビルド コマンドでの polyspace-configure の実行にかかる時間よりも大幅に短くなります。ただし、ユーザーは、指定するコンパイル データベースでソース コードの完全なビルドが正確に反映されていることを確認する必要があります。バージョン履歴
R2013b で導入