このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

polyspace-configure

(システム コマンド) DOS または UNIX コマンド ラインでビルド システムから Polyspace プロジェクトを作成

ページ内をすべて折りたたむ

構文

polyspace-configure buildCommand
polyspace-configure [options] buildCommand
polyspace-configure [options] -compilation-database jsonFile

説明

polyspace-configure システム コマンドは、ビルド コマンドから Polyspace® プロジェクトまたはオプション ファイルを作成します。

メモ

この Polyspace コマンドは polyspaceroot\polyspace\bin にあります。ここで、polyspaceroot は Polyspace インストール フォルダー (C:\Program Files\Polyspace\R2025a など) です (デスクトップ製品の場合はインストール フォルダー、サーバー製品の場合はインストール フォルダーも参照してください)。コマンドの絶対パスの入力を省略するには、この場所をオペレーティング システムの PATH 環境変数に追加します。

polyspace-configure buildCommand はビルド システムをトレースし、そのビルド システムから収集した情報によって Polyspace プロジェクトを作成します。Polyspace は、ビルド コマンドまたは makefile が一定の要件を満たしている場合にのみ、ビルド システムからプロジェクトを作成します。コンパイラおよびビルド コマンドの要件のリスト (Polyspace がサポートしているコンパイラのリストを含む) は、ビルド システムからのプロジェクト作成の要件を参照してください。

例

polyspace-configure [options] buildCommand はビルド システムをトレースし、options を使用して polyspace-configure の既定の動作を変更します。buildCommand の前に修飾子を指定します。指定しない場合、ビルド コマンド自体のオプションと見なされます。

例

polyspace-configure [options] -compilation-database jsonFile は、入力された JSON コンパイル データベース ファイル jsonFile から収集された情報を使用して Polyspace プロジェクトを作成します。ビルド コマンドを指定したり、ビルド システムをトレースしたりする必要はありません。JSON コンパイル データベースの詳細については、JSON Compilation Database を参照してください。

例

例

すべて折りたたむ

この例では、コンパイル コマンドを使用して Polyspace プロジェクトを作成する方法を示します。polyspace-configure を実行する最も簡単な方法は、ソース コードのビルドに使用するコンパイル コマンドで直接実行することです。この例では、GCC コンパイラとコンパイル コマンド gcc を使用します。GCC は、Linux® ベースのシステムに組み込まれている標準のコンパイラ スイートです。Windows® ベースのシステムの場合は、GCC コンパイラをサポートするために MinGW をインストールできます。

最初に、ソース コードがエラーなしでコンパイルされることを確認します。 

gcc myFilename.c otherFile.c
ソース コードがエラーなしでコンパイルされることを確認した後、続行する前にオブジェクト ファイルを削除します。
rm myFilename.o otherFile.o

一意のプロジェクト名を指定して Polyspace プロジェクトを作成します。以前にテストしたように、コンパイル コマンドで polyspace-configure を実行します。

polyspace-configure -prog myProject gcc myFilename.c otherFile.c

Polyspace プロジェクトを Polyspace ユーザー インターフェイスで開きます。

Visual Studio® を使用してソースをコンパイルする場合は、上記の例の gcc を cl に置き換えます。また、Visual Studio プロジェクトのフル ビルドで polyspace-configure を実行することもできます。Visual Studio ビルドからの Polyspace プロジェクトの作成を参照してください。

polyspace-configure では、コンパイル コマンドのソースを使用して新しい Polyspace プロジェクトが作成されることに注意してください。polyspace-configure コマンドを使用して、既に存在する Polyspace プロジェクトに追加することはできません。コンパイル オプション (gcc に対する -D など) を使用する場合、polyspace-configure によって、同等の Polyspace オプションがプロジェクトに設定されます。詳細は、アルゴリズムを参照してください。

この例では、コンパイル コマンドを使用して Polyspace Platform (Polyspace Test) プロジェクトを作成する方法を示します。polyspace-configure を実行する最も簡単な方法は、ソース コードのビルドに使用するコンパイル コマンドで直接実行することです。この例では、GCC コンパイラとコンパイル コマンド gcc を使用します。GCC は、Linux ベースのシステムに組み込まれている標準のコンパイラ スイートです。Windows ベースのシステムの場合は、GCC コンパイラをサポートするために MinGW をインストールできます。

最初に、ソース コードがエラーなしでコンパイルされることを確認します。 

gcc myFilename.c otherFile.c
ソース コードがエラーなしでコンパイルされることを確認した後、続行する前にオブジェクト ファイルを削除します。
rm myFilename.o otherFile.o

一意のプロジェクト名を指定して Polyspace Platform プロジェクトを作成します。以前にテストしたように、コンパイル コマンドで polyspace-configure を実行します。

polyspace-configure -output-platform-project myProject gcc myFilename.c otherFile.c

Polyspace プロジェクトを Polyspace Platform ユーザー インターフェイスで開きます。

Visual Studio を使用してソースをコンパイルする場合は、上記の例の gcc を cl に置き換えます。また、Visual Studio プロジェクトのフル ビルドで polyspace-configure を実行することもできます。Create Projects from Visual Studio in Polyspace Platform User Interface (Polyspace Test)を参照してください。

通常、実際のアプリケーションでは、コンパイラを直接呼び出してソース コードをビルドすることはありません。ビルド コマンドがいくつかのコマンドを実行し、そのうちの 1 つがコンパイルです。たとえば、makefile を実行してソース コードをビルドできます。この例では、コマンド make targetName buildOptions を使用してソース コードをビルドする場合に、Polyspace プロジェクトを作成する方法を示します。

一意のプロジェクト名を指定して Polyspace プロジェクトを作成します。makefile 内のすべての必要なターゲットが再作成されるように、make で -B オプションまたは -W makefileName オプションを使用します。

polyspace-configure  -prog myProject \
make -B targetName buildOptions

Polyspace プロジェクトを Polyspace ユーザー インターフェイスで開きます。

この例では、CMake ビルド システム ジェネレーターを使用して生成した JSON コンパイル データベースから Polyspace オプション ファイルを作成する方法を示します。CMake は、make 用の UNIX® Makefile や Microsoft® Visual Studio 用のプロジェクト ファイルなどの指定されたビルド ツールのビルド命令を生成します。CMake は、Makefile ジェネレーターと Ninja ジェネレーター専用の JSON コンパイル データベースの生成をサポートしています。詳細については、makefile generators を参照してください。

CMake プロジェクト用の JSON コンパイル データベースを生成します。Cmake プロジェクトの例については、polyspaceroot\polyspace\examples\doc_cxx\compilation_database を参照してください。ここで、polyspaceroot はPolyspace のインストール フォルダーです。

プロジェクト ソース ツリーのルートに移動します。このフォルダーには、CMake がビルド命令を生成するための入力として使用するファイル CMakeLists.txt が格納されています。次のコマンドを入力します。

mkdir JSON_cdb
cd JSON_cdb
cmake -G "Unix Makefiles" -DCMAKE_EXPORT_COMPILE_COMMANDS=1 ../
最後のコマンドは、make ビルド ツール用のビルド命令を使用して UNIX makefile を生成します。このコマンドは、ファイル compile_commands.json も出力します。このファイルでは、プロジェクト内のすべての翻訳単位のコンパイラ呼び出しが列挙されます。

以前のステップで生成したコンパイル データベースから Polyspace オプション ファイルを生成します。

polyspace-configure -compilation-database compile_commands.json \
-output-options-file options.txt
ビルド コマンドを指定する必要はなく、polyspace-configure はビルドをトレースしません。Polyspace が JSON コンパイル データベースからビルド システムに関する情報を抽出します。

次のように、Polyspace にオプション ファイルを渡して、解析を実行します。

polyspace-code-prover -options-file options.txt

この例では、ビルド システムの同じトレースから異なる Polyspace プロジェクトを作成する方法を示します。各プロジェクトに含めるソース ファイルを指定することができます。

オプション -no-project を指定すると、Polyspace プロジェクトを作成せずにビルド システムをトレースします。makefile 内のすべての必要なターゲットが再作成されるようにするには、-B など、適切な make ビルド コマンド オプションを使用します。

polyspace-configure -no-project make -B

polyspace-configure は、現在のフォルダー内の既定の場所にキャッシュ情報とビルド トレースを保存します。別の場所にキャッシュ情報とビルド トレースを保存するには、オプション -cache-path および -build-trace を指定します。

前のステップからのビルド トレース情報を使用して、Polyspace プロジェクトを生成します。各プロジェクトに含めるファイルを選択するには、プロジェクト名を指定して -include-sources または -exclude-sources オプションを使用します。

polyspace-configure -no-build -prog myProject \
-include-sources "glob_pattern"

glob_pattern は、フィルターしてプロジェクトに追加または除外するフォルダーまたはファイルに対応する glob パターンです。polyspace-configure に渡す glob パターンがシェルによって展開されないようにするには、glob パターンを二重引用符で囲みます。glob パターンでサポートされる構文の詳細は、パターン マッチングを使用した Polyspace 解析対象ファイルの選択を参照してください。

前のステップでオプション -build-trace および -cache-path を指定した場合、これらをもう一度指定します。

トレース ファイルとキャッシュ フォルダーを削除します。

rm -r polyspace_configure_cache polyspace_configure_build_trace
オプション -build-trace および -cache-path を使用した場合は、これらのオプションのパスとファイル名を使用します。

この例では、コマンド make targetName buildOptions を使用してソース コードをビルドする場合に、Polyspace 解析を実行する方法を示します。この例では、polyspace-configure を使用してビルド システムをトレースしますが、Polyspace プロジェクトは作成しません。その代わりに、コマンド ラインからの Polyspace 解析実行に使用できるオプション ファイルを作成します。

-output-options-file コマンドを指定して、Polyspace のオプション ファイルを作成します。makefile 内のすべての必要なターゲットが再作成されるように、make で -B オプションまたは -W makefileName オプションを使用します。

polyspace-configure -output-options-file\
 myOptions make -B targetName buildOptions

作成したオプション ファイルを使用して、Polyspace 解析をコマンド ラインで実行します。

polyspace-code-prover -options-file myOptions

入力引数

すべて折りたたむ

ソース コードのビルド用に合わせて指定されたビルド コマンド。

このビルド コマンドでは、ソースのインクリメンタル ビルドではなく、フル ビルドを実行する必要があります。通常、make などのビルド コマンドは、前回のビルド以降に変更されたソースだけをビルドするようにセットアップされています。しかし、polyspace-configure では、Polyspace プロジェクトまたはオプション ファイルに追加するソースを決定するために、フル ビルドが必要です。フル ビルドを強制するために適切なオプションをビルド コマンドに追加してください。たとえば、makefile を使用している場合は、オプション -B を make に追加します。

例: make -B, make -B -W makefileName

オプション説明
-prog projectName

Polyspace ユーザー インターフェイスに表示されるプロジェクト名。既定値は polyspace です。

オプション -output-project を使用しない場合は、-prog 引数によってプロジェクト名も設定されます。

例: -prog myProject は、ユーザー インターフェイスに myProject という名前が表示されるプロジェクトを作成します。オプション -output-project を使用しない場合は、プロジェクト名も myProject.psrprj になります。

-author authorName

プロジェクト作成者の名前。

例: -author jsmith

-output-project filePath

Polyspace プロジェクト ファイルのパス。既定値は現在のフォルダー内のファイル polyspace.psprj です。

例: -output-project ../myProjects/project1 は、プロジェクト project1.psprj を相対パス ../myProjects/ のフォルダーに作成します。

-output-platform-project filePath

Polyspace Platform プロジェクト ファイルまたはワークスペース ファイルのパス (オプション -module、-modules-list、-module-output-pattern のいずれかを使用している場合)。Polyspace は、このファイルを現在のフォルダー内に保存します。

例: -output-platform-project ../myProjects/project1 は、プロジェクト project1.psprjx を相対パス ../myProjects/ のフォルダーに作成します。

例: -output-platform-project ../myProjects/workspace1 -module は、ワークスペース ファイル project1.pswkps を相対パス ../myProjects/ のフォルダーに作成します。

Polyspace Platform プロジェクトの詳細については、以下を参照してください。

-update-platform-project filePath

このオプションは、現在のプロジェクト実行の構成を使用して、Polyspace Platform プロジェクト (.psprjx) のビルド構成を更新するために使用します。filePath 引数は相対パスまたは絶対パスとして指定できます。プロセッサ構成が既に存在する場合、このコマンドは新しいビルド構成にその構成を使用します。

指定されたプロジェクトが存在しない場合は、このコマンドは新しいプロジェクトを作成します。

例: polyspace-configure -update-platform-project ../myProjects/myProject.psprjx

-output-options-file filePath

Polyspace が生成する解析オプション ファイルのパス。このファイルは、以下のいずれかのコマンドを使用してコマンド ラインからの解析を行うために使用します。

  • polyspace-bug-finder

  • polyspace-code-prover

  • polyspace-bug-finder-server

  • polyspace-code-prover-server

  • polyspace-bug-finder-access

-allow-build-error

ビルド プロセスでエラーが発生しても Polyspace プロジェクトを作成するためのオプション。

エラーが発生した場合、ビルドのトレース ログには次のメッセージが示されます。

polyspace-configure (polyspaceConfigure) 
   ERROR: build command 
   command_name fail [status=status_value]
command_name は使用するビルド コマンド名、status_value はビルド プロセスでどのエラーが発生したのかを示す非ゼロの終了ステータスまたはエラー レベルです。

このオプションでは、ビルド コマンドによりソース ファイルがビルドされるが、ビルド コマンドがゼロ以外の終了ステータスで終了する場合に、有用なプロジェクトを作成できます。ソース ファイルがコンパイルされず、ビルドが失敗する場合は、polyspace-configure を再び使用する前にビルドの失敗を解決してください。

-compilation-database が使用されている場合は、このオプションが無視されます。

-allow-overwrite

同じ名前のプロジェクトが既に存在する場合、プロジェクトを上書きするオプション。

既定では、出力フォルダーに同じ名前のプロジェクトが既に存在する場合、polyspace-configure (polyspaceConfigure) でエラーが発生します。このオプションを使用してプロジェクトを上書きします。

-no-console-output

-silent (既定の設定)

-verbose

polyspace-configure (polyspaceConfigure) の実行による詳しいメッセージを表示または非表示にするオプション。

  • -no-console-output – エラーと警告を含む、すべての出力を非表示にします。

  • -silent (既定) — エラーと警告のみを表示します。

  • -verbose – すべてのメッセージを表示します。

複数のオプションを指定した場合、最も詳細な表示オプションが適用されます。

-easy-debug と組み合わせて使用されている場合、Polyspace はこれらのオプションを無視します。

-help

polyspace-configure (polyspaceConfigure) コマンドの完全なリストを表示するオプション

-debug

MathWorks® テクニカル サポートが使用するデバッグ情報を保存するオプション。

このオプションは、オプション -easy-debug によって置き換えられました。

-easy-debug folderPath

MathWorks テクニカル サポートで使用するデバッグ情報が Polyspace によって保存されているフォルダーのパス。

polyspace-configure (polyspaceConfigure) の実行後、folderPath フォルダーに名前が pscfg-output.zip で終わる圧縮ファイルが格納されます。実行時に完全な Polyspace プロジェクトまたはオプション ファイルが作成されない場合は、詳細なデバッグを行うため、この圧縮ファイルを MathWorks テクニカル サポートに送信してください。この圧縮ファイルには、ビルドで追跡されたソース ファイルは含まれていません。ビルド システムからのプロジェクトの作成におけるエラーも参照してください。

オプション説明
-module

ビルド システムで作成するバイナリごとに個別の解析モジュールを作成するオプション。

解析モジュールを構成する内容は、polyspace-configure コマンドの出力に応じて異なります。

  • オプション -module をオプション -output-project projectName と併せて使用すると、このコマンドはバイナリごとに、1 つのモジュールを持つ 1 つのファイル projectName.psprj を作成します。

  • オプション -module をオプション -output-options-path pathName と併せて使用すると、このコマンドはバイナリごとに 1 つのオプション ファイルをフォルダー pathName に作成します。

  • オプション -module をオプション -output-platform-project workspaceName と併せて使用すると、Polyspace はワークスペース ファイル (workspaceName.pswks) と、バイナリごとに 1 つの Polyspace Platform プロジェクト (.psprjx) を作成します。ワークスペースの詳細については、Manage Related Projects in Polyspace Platform User Interface Using Workspacesを参照してください。

このオプションは以下のケースでのみサポートされています。

  • 次のいずれかのリンカーを使用してビルド コマンドからプロジェクトまたはオプション ファイルを作成する場合。

    • GNU® — ld、gold、または ar リンカー。

    • Visual C++® — link.exe リンカー。

  • CMake JSON コンパイル データベースからプロジェクトまたはオプション ファイルを作成する場合。

この方法でバイナリごとに個別のオプション ファイルを作成する場合、各オプション ファイルには、共有オブジェクトを介したものではなく、バイナリに直接関連するソース ファイルが含まれることに注意してください。詳細は、ビルド コマンドを使用した Polyspace 解析のモジュール化を参照してください。

-modules-list fileWithModuleList

テキスト ファイル fileWithModuleList に指定したルート フォルダーごとに個別の出力を作成するオプション。テキスト ファイルでルート フォルダーを 1 行に 1 つずつ指定します。テキスト ファイルにリストされているルート フォルダーごとに、polyspace-configure コマンドはそのルート フォルダー内のソース ファイルのみからなる個別の解析モジュールを作成します。オプション -project-root を使用していない場合は、ルート フォルダーのパスは現在の作業フォルダーを基準にして解決されます。

解析モジュールを構成する内容は、polyspace-configure コマンドの出力に応じて異なります。

  • オプション -modules-list をオプション -output-options-path pathName と併せて使用すると、コマンドはルート フォルダーごとに 1 つのオプション ファイルをフォルダー pathName に作成します。

  • オプション -modules-list をオプション -output-platform-project workspaceName と併せて使用すると、Polyspace はワークスペース ファイル (workspaceName.pswks) と、ルート フォルダーごとに 1 つの Polyspace Platform プロジェクト (.psprjx) を作成します。ワークスペースの詳細については、Manage Related Projects in Polyspace Platform User Interface Using Workspacesを参照してください。

このオプションは、プロジェクトまたはオプション ファイルを、ビルド コマンドと JSON コンパイル データベースのいずれから作成する場合にもサポートされます。

-module-output-pattern regex

正規表現 regex によりキャプチャされるルート フォルダーごとに個別の出力を作成するオプション。正規表現でキャプチャ対象グループを指定します。正規表現によりキャプチャされるルート フォルダーごとに、polyspace-configure コマンドはそのルート フォルダーのソース ファイルのみからなる個別の解析モジュールを作成します。ルート フォルダー パスは次のように解決されます。

  • ビルド コマンドから解析モジュールを作成する場合は、ビルド コマンドの実行元のフォルダーを基準にします。

  • JSON コンパイル データベースから解析モジュールを作成する場合は、JSON コンパイル データベースの directory エントリを基準にします。

解析モジュールを構成する内容は、polyspace-configure コマンドの出力に応じて異なります。

  • オプション -module-output-pattern をオプション -output-options-path pathName と併せて使用すると、コマンドはルート フォルダーごとに 1 つのオプション ファイルをフォルダー pathName に作成します。

  • オプション -module-output-pattern をオプション -output-platform-project workspaceName と併せて使用すると、Polyspace はワークスペース ファイル (workspaceName.pswks) と、ルート フォルダーごとに 1 つの Polyspace Platform プロジェクト (.psprjx) を作成します。ワークスペースの詳細については、Manage Related Projects in Polyspace Platform User Interface Using Workspacesを参照してください。

このオプションは、プロジェクトまたはオプション ファイルを、ビルド コマンドと JSON コンパイル データベースのいずれから作成する場合にもサポートされます。

-output-options-path folderPath

生成されたオプション ファイルを保存するフォルダーのパス。オプション -module または -modules-list と一緒にこのオプションを使用します。

オプション ファイルには、ビルド システムで作成されるバイナリに由来した名前が付けられます。

-project-root folderPathルート フォルダー パスの解決の基準となるフォルダーのパス。オプション -modules-list と一緒にこのオプションを使用します。このオプションを省略すると、-modules-list で指定されるテキスト ファイルのルート フォルダー パスは、現在の作業フォルダーを基準にして解決されます。
オプション説明
-compilation-database filePath

JSON コンパイル データベース (JSON CDB) ファイルのパス。このファイルは、たとえば、cmake と一緒にフラグ -DCMAKE_EXPORT_COMPILE_COMMANDS=1 を使用することによって、ビルド システムから生成します。このファイルには、プロジェクト内のすべての翻訳単位のコンパイラ呼び出しが含まれています。詳細については、JSON Compilation Database を参照してください。polyspace-configure は、このファイルの内容を使用してビルド システムに関する情報を入手します。JSON CDB 内の抽出されたコンパイラ パスは、polyspace-configure を実行するパスからアクセスできる必要があります。

このオプションを使用する場合は、ビルド コマンドを指定しません。

以下のビルド システムとコンパイラは JSON CDB の生成をサポートしています。

  • CMake

  • Bazel

  • Clang

  • Ninja

  • Qbs

  • waf

このオプションは、-no-project および複数のモジュールを作成するためのオプションと互換性がありません。

このオプションが使用されている場合、Polyspace はキャッシュ管理オプションの -allow-build-error と -no-build を無視します。

-compiler-config filePath

コンパイラ構成ファイルのパス。

ファイルは指定された形式でなければなりません。参考として、polyspaceroot\polyspace\configure\compiler_configuration\ の既存の構成ファイルをご覧ください。ファイルのコンテンツに関する詳細は、サポートされていないコンパイラを使用するビルド システムからの Polyspace プロジェクトの作成を参照してください。

例: -compiler-config myCompiler.xml

-no-project

Polyspace プロジェクトを作成せずにビルド システムをトレースし、ビルド トレース情報を保存するオプション。

このオプションは、後ほど -no-build オプションを指定して polyspace-configure (polyspaceConfigure) を実行するための、ビルド トレース情報を保存するために使用します。

このオプションは、-compilation-database と互換性がありません。

-no-build

以前保存したビルド トレース情報を使用して Polyspace プロジェクトを作成するオプション。

このオプションを使用するには、以前に -no-project オプションを指定した polyspace-configure (polyspaceConfigure) の実行によって保存された、ビルド トレース情報がなければなりません。

このオプションを使用する場合、buildCommand 引数を指定する必要はありません。

-compilation-database が使用されている場合は、このオプションが無視されます。

-no-sources

ソース ファイル指定が含まれていない Polyspace オプション ファイルを作成するオプション。

他の手段でソース ファイルを指定する意図がある場合、このオプションを使用します。たとえば、次の場合にこのオプションを使用できます。

  • AUTOSAR 固有のコードに対する Polyspace の実行。

    コンパイラ オプションについてビルド コマンドをトレースするオプション ファイルを作成するとします。

    -output-options-file options.txt -no-sources
    ARXML 仕様からソース ファイル名を抽出し、polyspace-autosar を使用して以降の Code Prover 解析を実行するときに、このオプション ファイルを後から追加します。
    -extra-options-file options.txt

    ビルド コマンドを使用した AUTOSAR コードに対する Polyspace の実行も参照してください。

  • Eclipse™ での Polyspace の実行。

    ソース ファイルは既に Eclipse プロジェクトで指定されています。Polyspace 解析を実行する場合、コンパイル オプションのみを含むオプション ファイルを指定する必要があります。

-extra-project-options polyspaceAnalysisOpts

以降の Polyspace 解析に使用するオプション。

Polyspace プロジェクトを作成すると、そのプロジェクトの既定のオプションの一部を変更できます。または、ビルド コマンドをトレースするときに、これらのオプションを渡すことができます。フラグ -extra-project-options により、追加オプションを渡すことができます。

"-allow-negative-operand-in-shift -stubbed-pointers-are-unsafe" のように、スペース区切りのリストで複数のオプションを指定します。

作成したすべての Polyspace プロジェクトにオプション -stubbed-pointers-are-unsafe を設定しなければならないとします。各プロジェクトを開いてこのオプションを設定する代わりに、Polyspace プロジェクトを作成するときに次のフラグを使用できます。

-extra-project-options "-stubbed-pointers-are-unsafe"

使用可能なオプションのリストは、以下を参照してください。

ビルド コマンドから Polyspace プロジェクトの代わりにオプション ファイルを作成する場合、このフラグは使用しないでください。代わりに、解析開始時に、生成したオプション ファイル、個別のオプション ファイル、またはコマンド ラインで、解析オプションを手動で追加します。

-tmp-path folderPath一時ファイルを保存するフォルダーのパス。
-build-trace filePath

ビルド情報を保存するファイルのパス。既定値は ./polyspace_configure_build_trace.log です。

例: -build-trace ../build_info/trace.log

-log filePath polyspace-configure コマンドの出力を保存するログ ファイルのパス。このオプションの使用はコンソール出力を抑止しません。

-include-sources glob pattern

-exclude-sources glob pattern

polyspace-configure (polyspaceConfigure) によって、生成されるプロジェクトに追加または生成されるプロジェクトから除外するソース ファイルを指定するオプション。両方のオプションを組み合わせることができます。

このファイル パスが、-include-sources に渡す glob pattern と一致する場合、ソース ファイルがインクルードされます。

このファイル パスが、-exclude-sources に渡す glob pattern と一致する場合、ソース ファイルが除外されます。

-print-included-sources

-print-excluded-sources

polyspace-configure (polyspaceConfigure) によって、生成されるプロジェクトに追加または生成されるプロジェクトから除外するソース ファイルのリストを出力するオプション。両方のオプションを組み合わせることができます。出力には、個別の行に各ファイルの絶対パスが表示されます。

-include-sources または -exclude-sources に渡す glob パターンをトラブルシューティングするには、このオプションを使用します。-include-sources または -exclude-sources に渡すパターンと一致するファイルを確認できます。

-compiler-cache-path folderPath

polyspace-configure がコンパイラ キャッシュ ファイルを検索または保存するフォルダー パスを指定します。このフォルダーが存在しない場合は、polyspace-configure によって作成されます。

既定で、Polyspace は、以下のフォルダー パスの下でコンパイラ キャッシュを検索または保存します。

  • Windows

    %appdata%\Mathworks\R2025a\Polyspace

  • Linux

    ~/.matlab/R2025a/Polyspace

  • Mac

    ~/Library/Application Support/MathWorks/MATLAB/R2025a/Polyspace

-no-compiler-cache

このオプションは、Polyspace がコンパイラ構成情報をキャッシュしないようにまたは既存のキャッシュをコンパイラ構成で使用しないようにする場合に使用します。

既定で、特定のコンパイラ構成を使用して、初めて、polyspace-configure を実行すると、Polyspace がコンパイラに基本型のサイズ、コンパイラ マクロ定義、およびその他のコンパイラ構成情報を問い合わせてから、その情報をキャッシュします。Polyspace は、同じコンパイラ構成を使用するビルド用の polyspace-configure の以降の実行でキャッシュされた情報を再利用します。

-reset-compiler-cache-entryこのオプションは、コンパイラに現在の構成を問い合わせ、その構成に対応するキャッシュ ファイル内のエントリをアップデートするために使用します。キャッシュ内のその他のコンパイラ構成エントリはアップデートされません。
-clear-compiler-cache

このオプションは、キャッシュ ファイルに保存されたすべてのコンパイラ構成を削除するために使用します。

ビルド コマンドまたは -compilation-database も指定した場合は、polyspace-configure が、-no-project または -no-compiler-cache が指定された場合を除いて、現在の実行のコンパイラ構成情報を計算してキャッシュします。

-import-macro-definitions none | from-allowlist | from-source-tokens | from-compiler

通常、このオプションを指定する必要はありません。

Polyspace は、次の優先順位に従ってコンパイラにマクロ定義を問い合わせるための最良の手法を自動的に判断します。

  1. from-compiler — Polyspace は gcc -dm -E などのネイティブ コンパイラ オプションを使用して、コンパイラ マクロ定義を取得します。この手法では、ビルドをトレースするために Polyspace を必要としません。この手法は、マクロ定義のリストをサポートしているコンパイラでのみ利用可能です。

  2. from-source-tokens — Polyspace は、ソース コード内のすべての非キーワード トークンを使用して、コンパイラにマクロ定義を問い合わせます。この手法は、Polyspace がビルドをトレースできる場合にのみ利用できます。-compilation-database オプションを使用する場合は、この手法は利用できません。

  3. from-allowlist — Polyspace は、内部の許可リストを使用してコンパイラにマクロ定義を問い合わせます。

マクロ定義を手動で指定する場合は、このオプションと none フラグを使用し、またオプション [プリプロセッサ定義] (-D) を使用してマクロ定義を指定します。

Polyspace で使用されるマクロ インポート手法が目的の手法と異なる場合は、このオプションを手動で指定して、問題のトラブルシューティングを行ってください。

-options-for-sources-delimiter delimCharacter

Polyspace がオプション -options-for-sources を使用してソース ファイルに関連付けられたオプション ファイルを生成するときに、解析オプションの間の区切り文字として使用する文字を指定します。通常、オプション -options-for-sources では、生成されるファイル内で解析オプションの間の区切り文字として ; 文字 (セミコロン) を使用します。

-options-for-sources も参照してください。

これらのオプションは、主にデバッグに役立ちます。これらのオプションは、polyspace-configure (polyspaceConfigure) が失敗し、MathWorks テクニカル サポートからこのオプションを使用してキャッシュされたファイルを提供するように求められた場合に使用します。R2020a 以降では、オプション -easy-debug を使用してデバッグ情報をより簡単に提供できます。Polyspace 実行時の問題に関するテクニカル サポートへのお問い合わせを参照してください。

-compilation-database が使用されている場合、Polyspace はこれらのオプションを無視します。

オプション説明

-no-cache

-cache-sources (既定の設定)

-cache-all-text

-cache-all-files

以下のいずれかを実行するオプション:

  • -no-cache:キャッシュを作成しない

  • -cache-sources:ビルド中に polyspace-configure (polyspaceConfigure) による後の利用に向けて一時的に作成されたテキスト ファイルをキャッシュ

  • -cache-all-text:ソースおよびヘッダーを含むすべてのテキスト ファイルをキャッシュ

  • -cache-all-files:バイナリを含むすべてのファイルをキャッシュ

通常、ビルド コマンドによって作成された一時ファイルをキャッシュするのは、コマンドのトレース時における問題をデバッグするためです。

-cache-path folderPath

キャッシュ情報を保存するフォルダーのパス。

Visual Studio ビルド (devenv.exe) のトレース中にエラーが表示された場合:

path is too long
エラーを回避するためにこのオプションの短い方のパスの使用を試します。

例: -cache-path ../cache

-keep-cache

-no-keep-cache (既定の設定)

polyspace-configure (polyspaceConfigure) の実行の完了後にキャッシュ情報を保持またはクリーンアップするオプション。

polyspace-configure (polyspaceConfigure) が失敗した場合は、このキャッシュ情報をデバッグの目的でテクニカル サポートに提供できます。

アルゴリズム

polyspace-configure コマンドは、おおまかに次の手順で make などのビルド コマンドから Polyspace プロジェクトまたはオプション ファイルを作成します。

  1. ビルド コマンドが最初に実行されます。polyspace-configure は、このビルドで実行されるコマンド、読み取られたファイル、書き込まれたファイルを追跡します。これらのコマンドの 1 つ以上がコンパイラを呼び出します。たとえば、ビルド コマンドが GCC コンパイラを使用する場合、これらのコマンドの 1 つ以上が gcc、g++、または関連する実行可能ファイルを実行します。既知のコンパイラ実行可能ファイルが存在しているかどうかに応じて、polyspace-configure はビルド中に実行されたすべてのコマンドの中から、コンパイラ呼び出しコマンドを選択します。

  2. 各コンパイラ呼び出しコマンドは、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 で導入

参考

トピック