メインコンテンツ

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

polyspaceConfigure

MATLAB コマンド ラインでビルド システムから Polyspace プロジェクトを作成

説明

polyspaceConfigure buildCommand はビルド システムをトレースし、そこから収集した情報によって Polyspace® プロジェクトを作成します。Polyspace デスクトップ製品のユーザー インターフェイスでのみ Polyspace プロジェクトの解析を実行できます。

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

メモ

MATLAB® から Polyspace を実行する前に、Polyspace インストールと MATLAB インストールをリンクしなければなりません。MATLAB や Simulink との Polyspace の統合またはPolyspace Server 製品と MATLAB との統合を参照してください。

すべて折りたたむ

この例では、コマンド make targetName buildOptions を使用してソース コードをビルドする場合に、Polyspace プロジェクトを作成する方法を示します。この例では、Polyspace デスクトップ製品のユーザー インターフェイスでのみ開くことができる Polyspace プロジェクトを作成します。

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

polyspaceConfigure  -prog myProject ...
          make -B targetName buildOptions

Polyspace プロジェクトを [プロジェクト ブラウザー] で開きます。

polyspaceCodeProver('myProject.psprj') 

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

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

polyspaceConfigure -no-project make -B;

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

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

polyspaceConfigure -no-build -prog myProject ...
-include-sources "glob_pattern";

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

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

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

rmdir('polyspace_configure_cache', 's');
delete polyspace_configure_built_trace;
 
オプション -build-trace および -cache-path を使用した場合は、これらのオプションのパスとファイル名を使用します。

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

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

polyspaceConfigure -output-options-file ... 
         myOptions make -B targetName buildOptions

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

polyspaceCodeProver -options-file myOptions

入力引数

すべて折りたたむ

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

例: make -B, make -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®ldgold、または 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) が失敗した場合は、このキャッシュ情報をデバッグの目的でテクニカル サポートに提供できます。

バージョン履歴

R2013b で導入