このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。
ユーザー インターフェイスでの Polyspace 解析オプションの設定とスクリプトの生成
デスクトップ製品の Polyspace® Bug Finder™ や Polyspace Code Prover™ がインストールされている場合、デスクトップ製品のユーザー インターフェイスでプロジェクトを構成できます。その後、ユーザー インターフェイスで定義した構成からスクリプトまたはオプション ファイルを生成し、デスクトップ製品またはサーバー製品での自動実行のために、そのスクリプトまたはオプション ファイルを使用できます。
ビルド コマンドなど既存の仕様から Polyspace プロジェクトを作成する場合を除き、プロジェクトを設定する際、最初に数回試行しなければならないことがあります。このような試行で、コンパイル エラーが発生したりコードがチェックされなかったりする場合、解析構成を変更しなければならない可能性があります。デスクトップ製品のユーザー インターフェイスで、この初期設定を実行するのは簡単です。ユーザー インターフェイスには、次のようなさまざまな機能が用意されています。
制約指定のための XML ファイルの自動生成。
オプションに関する状況依存のヘルプ。
前提条件
Polyspace ユーザー インターフェイスを開き、オプションを設定するには、少なくとも Polyspace Bug Finder と Polyspace Code Prover のいずれかのライセンスがなければなりません。
スクリプトを生成した後、デスクトップ製品 (Polyspace Bug Finder および Polyspace Code Prover) またはサーバー製品 (Polyspace Bug Finder Server™ や Polyspace Code Prover Server) を使用して解析を実行できます。
構成からのスクリプトの生成
この例では、Bug Finder の構成からスクリプトを生成する方法を示します。同じ手順を Code Prover の構成にも適用できます。
Polyspace ユーザー インターフェイスでソース ファイルを新しいプロジェクトに追加します。
polyspaceroot\polyspace\binpolyspacerootC:\Program Files\Polyspace\R2025aです。polyspace実行可能ファイルを使用して Polyspace ユーザー インターフェイスを開き、新しいプロジェクトを作成します。ユーザー インターフェイスでの Polyspace の実行を参照してください。
Polyspace プロジェクトの [構成] ペインで解析オプションを指定します。このペインを開くには、プロジェクト ブラウザーで Polyspace プロジェクトの構成ノードをクリックします。
Polyspace 解析オプションの指定を参照してください。
解析を実行します。コンパイル エラーと解析結果に基づいて、必要に応じてオプションを変更します。
Polyspace ユーザー インターフェイスでの静的解析の実行を参照してください。
解析オプションを設定したら、プロジェクト (
.psprjファイル) からスクリプトを生成します。デモ プロジェクト
Bug_Finder_Exampleからスクリプトを生成するには、次のようにします。プロジェクトを読み込みます。[ヘルプ] 、 [例] 、 [Bug_Finder_Example.psprj] を選択します。このプロジェクトのコピーが既定のワークスペースの
Examplesフォルダーに読み込まれます。プロジェクトの場所を見つけるために、[プロジェクト ブラウザー] ペインのプロジェクト名の上にカーソルを置きます。プロジェクトの場所に移動し、以下を入力します。
polyspace -generate-launching-script-for Bug_Finder_Example.psprj -bug-finder
Code Prover スクリプトを生成するには、
-bug-finderオプションなしで同じコマンドを使用します。プロジェクトに (それぞれが複数の構成をもつ) 複数のモジュールがある場合、現在アクティブなモジュールにおける現在アクティブな構成のオプションは、スクリプト内で抽出されることになります。
解析のスクリプト化用に、以下のファイルが生成されます。
source_command.txt:ソース ファイルをリストします。このファイルは-sources-list-fileオプションの引数として指定できます。options_command.txt:解析オプションをリストします。このファイルは-options-fileオプションの引数として指定できます。launchingCommand.batまたはlaunchingCommand.sh(オペレーティング システムにより異なる)。このファイルはpolyspace-bug-finderまたはpolyspace-code-prover実行可能ファイルを使用して解析を実行します。解析は、source_command.txtにリストされているソース ファイルに対して実行され、options_command.txtにリストされているオプションを使用します。
生成されたスクリプトを使用した解析の実行
解析を設定してスクリプトを生成した後、生成されたファイルを使用して以降の解析を自動化できます。デスクトップ製品またはサーバー製品を使用して以降の解析を自動化できます。
デスクトップ製品 Polyspace Bug Finder を使用して Bug Finder 解析を自動化するには、次のようにします。
前の節で説明したようにスクリプトを生成します。
定期的な間隔でまたは事前定義されたトリガーに基づいて、スクリプト
launchingCommand.batまたはlaunchingCommand.shを実行します。
サーバー製品 Polyspace Bug Finder Server を使用して Bug Finder 解析を自動化するには、次のようにします。
ユーザー インターフェイスでオプションを指定した後、スクリプトを生成する前に、サーバー製品が動作しているサーバーに Polyspace プロジェクト (
.psprjファイル) を移動します。前の節で説明したようにスクリプトを生成します。
このスクリプトは、デスクトップ製品ではなくサーバー製品の実行可能ファイルを参照します。
定期的な間隔でまたは事前定義されたトリガーに基づいて、スクリプト
launchingCommand.batまたはlaunchingCommand.shを実行します。
または、デスクトップ製品用に生成されたスクリプトをサーバー製品で実行するように変更できます。このスクリプトは、次のようなデスクトップ製品の実行可能ファイルへのパスを参照しています。
"C:\Program Files\Polyspace\R2025a\polyspace\bin\polyspace-code-prover.exe""C:\Program Files\Polyspace Server\R2025a\polyspace\bin\polyspace-code-prover-server.exe"場合によっては、オプション ファイルの一部のオプションのオーバーライドが必要になることがあります。たとえば、結果フォルダーを指定するオプションはスクリプト内にハードコードされています。スクリプトを起動する際に、このオプションを削除するかオーバーライドすることができます。
launchingCommand -results-dir newResultsFolder
newResultsFolderoptions_command.txt の複数のオプションをオーバーライドする場合、別のオプション ファイルにオーバーライド内容を保存できます。両方のオプション ファイルが使用されるように、スクリプト launchingCommand.bat または launchingCommand.sh を変更します。このスクリプトでは、オプション ファイルを使用するために、次のようにオプション -options-file を使用しています。
-options-file options_command.txt
overrides.txt に配置する場合は、スクリプトを変更して、もう 1 つの -options-file オプションを追加します。-options-file options_command.txt -options-file overrides.txt
