サーバーでの Polyspace Code Prover の実行と Web インターフェイスへの結果のアップロード

Polyspace^® Code Prover™ Server™ は、C/C++ コードにランタイム エラーがないことを証明し、コード レビューのために調査結果を Web インターフェイスにアップロードします。

継続的インテグレーションの一環として Code Prover を実行できます。Code Prover 解析を定期的に実行、または新しいコード送信に基づいて実行するスクリプトを設定します。これらのスクリプトは、Polyspace Web インターフェイスでのレビューのために解析結果をアップロードし、オプションでソース ファイルのオーナーに Polyspace の調査結果を記載したメールを送信します。オーナーは Web インターフェイスを開いて、送信された新しい調査結果のみをレビューし、問題を修正したり正当化したりできます。

一般的なプロジェクトまたはチームでは、Polyspace Code Prover Server がいくつかのテスト サーバーで定期的に実行され、レビューのために結果をアップロードします。チームの開発者と品質エンジニアの各々が Polyspace Access™ のライセンスを所有し、Web インターフェイスで結果を表示して調査とバグ修正を行います。

前提条件

サーバーで Code Prover 解析を実行し、Polyspace Access Web インターフェイスで結果を確認するには、次の 1 回限りの設定を実行します。

• 解析を実行するには、Polyspace Code Prover Server 製品のインスタンスを 1 つインストールします。

• 結果をアップロードするには、Polyspace Access Web インターフェイスをホストするために必要なコンポーネントを設定します。

• アップロードされた結果を表示するには、結果をレビューする開発者の各々が Polyspace Access のライセンスを所有していなければなりません。

Polyspace Server および Access 製品のインストールを参照してください。

Polyspace インストールのチェック

Polyspace Code Prover Server がインストールされているかどうかを確認するには、次のようにします。

1. コマンド ウィンドウを開きます。polyspaceserverroot\polyspace\bin に移動します。ここで、polyspaceserverroot は Polyspace Code Prover Server インストール フォルダーです。たとえば、C:\Program Files\Polyspace Server\R2025b です。インストール フォルダーも参照してください。

2. 以下を入力します。

   polyspace-code-prover-server -help

Code Prover 解析で使用できるオプションのリストが表示されます。

Polyspace Web インターフェイスがアップロード用に設定されているかどうかをチェックするには、次のようにします。

1. 再度 polyspaceserverroot\polyspace\bin に移動します。

2. 以下を入力します。

   polyspace-access -host <hostName> -port <portNumber> -create-project testProject

   ここで、hostName は Polyspace Access Web サーバーをホストしているサーバーの名前です。ローカルでホストされているサーバーの場合は localhost を使用します。portNumber は、サーバーのポート番号 (オプション) です。ポート番号を省略した場合、9443 が使用されます。

   設定が完了すると、testProject という名前のプロジェクトが Polyspace Web インターフェイスで作成されます。

   polyspace-access コマンドを使用するたびに、ログイン名とパスワードの入力を求められます。毎回ログイン情報を入力しないようにするには、ログイン名とパスワードの暗号化バージョンをコマンドで提供します。暗号化されたパスワードを作成するには、次のように入力します。

   polyspace-access -encrypt-password

   ログイン名とパスワードを入力します。暗号化されたパスワードをコピーし、polyspace-access コマンドを使用するときに -encrypted-password オプションとこの暗号化パスワードを指定します。

3. Web ブラウザーで、次の URL を開きます。

   https://<hostName>:<portNumber>/metrics/index.html

   ここで、hostName と portNumber は、前の手順で使用したホスト名とポート番号です。

Polyspace Web インターフェイスの [プロジェクト エクスプローラー] ペインに、新しく作成されたプロジェクト testProject が表示されます。

サンプル ファイルでの Code Prover の実行

Code Prover を実行するには、オペレーティング システムでコマンド ウィンドウを開きます。

1. Code Prover 解析を実行する場合は、polyspace-code-prover-server コマンドを使用します。

2. Polyspace Access Web インターフェイスでプロジェクト フォルダーを作成するには、polyspace-access -create-project (Polyspace Access) コマンドを使用します。

3. 結果をプロジェクトにアップロードするには、polyspace-access -upload (Polyspace Access) コマンドを使用します。

コマンドへの絶対パスの入力を省略するには、パス polyspaceserverroot\polyspace\bin をオペレーティング システムの Path 環境変数に追加します。

Polyspace インストールで提供されるサンプル ファイルのコマンドを試します。

1. サンプル ソース ファイルを polyspaceserverroot\polyspace\examples\cxx\Code_Prover_Example\sources から書き込み権限のある別のフォルダーにコピーします。コマンド ラインでこのフォルダーに移動します。

2. 以下を入力します。

   polyspace-code-prover-server -sources example.c,single_file_analysis.c -I . -main-generator -results-dir .
   polyspace-access -host <hostName> -port <portNumber> -login <username> -encrypted-password <pwd> -create-project testProject
   polyspace-access -host <hostName> -port <portNumber><portNumber> -login <username> -encrypted-password <pwd> -upload . -project myFirstProject -parent-project testProject

   ここで、username はログイン名、pwd は以前に作成した暗号化パスワードです。Polyspace インストールのチェックを参照してください。

Polyspace Web インターフェイスを更新します。[プロジェクト エクスプローラー] ペインの testProject フォルダーの下に、新しくアップロードされた結果が表示されます。

プロジェクトの結果を確認するには、[レビュー] をクリックします。詳細については、Web ブラウザーでの Polyspace Code Prover の結果のレビューを参照してください。Polyspace Access インターフェイスの右上にある ボタンを使用してドキュメントにアクセスすることもできます。

polyspace-code-prover-server コマンドで使用されるオプションは次のとおりです。

• -sources:コンマ区切りのソース ファイルを指定します。

• -I: インクルード フォルダーのパスを指定します。別のインクルード フォルダーを追加するたびに -I フラグを使用します。

• -results-dir: Polyspace Code Prover の結果を保存するフォルダーへのパスを指定します。

  実行されるたびに結果フォルダーがクリーンアップされて再設定されることに注意してください。クリーンアップ中にファイルが誤って削除されないようにするには、他のファイルを含む既存のフォルダーを使用するのではなく、Polyspace の結果専用のフォルダーを指定します。

• モジュールまたはライブラリの検証 (-main-generator):main 関数がソース ファイルにない場合に生成されなければならないことを指定します。

Code Prover の解析で使用できるすべてのオプションのリストについては、すべての Polyspace Code Prover 解析オプションのリストを参照してください。システムの Web ブラウザーで Code Prover ドキュメンテーションを開くには、次のように入力します。

polyspace-code-prover-server -doc

サーバーでの Code Prover 解析用のサンプル スクリプト

解析を実行するために、コマンド ラインでコマンドを入力する代わりにスクリプトを使用できます。スクリプトは、ソース ファイルを追加または変更するたびに実行します。

Windows^® バッチ ファイルのサンプルを以下に示します。ここでは、Polyspace インストールへのパスをスクリプトで指定しています。このスクリプトを使用するには、polyspaceserverroot をインストールへのパスに置き換えます。スクリプトで使用する暗号化パスワードは生成済みでなければなければなりません。Polyspace インストールのチェックを参照してください。

echo off
set POLYSPACE_PATH=polyspaceserverroot\polyspace\bin
set LOGIN=-host hostName -port portNumber -login <username> -encrypted-password <pwd>
"%POLYSPACE_PATH%\polyspace-code-prover-server" -sources example.c,single_file_analysis.c -I .^
 -main-generator -results-dir .
"%POLYSPACE_PATH%\polyspace-access" %LOGIN% -create-project testProject
"%POLYSPACE_PATH%\polyspace-access" %LOGIN% -upload . -project myFirstProject -parent-project testProject
pause

Linux^® シェル スクリプトのサンプルを以下に示します。

POLYSPACE_PATH=polyspaceserverroot/polyspace/bin
LOGIN=-host hostName -port portNumber -login <username> -encrypted-password <pwd>
${POLYSPACE_PATH}/polyspace-code-prover-server -sources example.c,single_file_analysis.c -I .\
 -main-generator -results-dir .
${POLYSPACE_PATH}/polyspace-access $LOGIN -create-project testProject
${POLYSPACE_PATH}/polyspace-access $LOGIN -upload . -project myFirstProject -parent-project testProject

起動スクリプトとは別のファイルでのソースおよびオプションの指定

ソース ファイルと解析オプションを起動スクリプト内でリスト指定する代わりに、それらを個別のテキスト ファイルでリスト指定できます。

• オプション -sources-list-file を使用して、ソースをリストしたテキスト ファイルを指定します。

• オプション -options-file を使用して、解析オプションをリストしたテキスト ファイルを指定します。

起動スクリプトからソース ファイルと解析オプションの指定を削除することにより、起動スクリプトを変更せずに、新しいコード送信で必要に応じてこれらの指定を変更できます。

前の例のスクリプトについて考えてみます。polyspace-code-prover-server コマンドを変更して、ソースとオプションを指定するテキスト ファイルを使用できます。以下のようにはしません。

polyspace-code-prover-server -sources example.c,single_file_analysis.c -I . -main-generator -results-dir .

以下を使用します。

polyspace-code-prover-server -sources-list-file sources.txt -options-file polyspace_opts.txt -results-dir .

ここで、以下となります。

• sources.txt には、以下のソース ファイルがリストされています。

  example.c
  single_file_analysis.c

• polyspace_opts.txt には、解析オプションが別々の行にリストされています。

  -I .
  -main-generator

通常、ソース ファイルはビルド コマンド (makefile) で指定されます。ソース ファイルを直接指定する代わりに、ビルド コマンドをトレースしてソース指定のリストを作成できます。polyspace-configure を参照してください。

全体のワークフロー

一般的な継続的インテグレーション ワークフローでは、次の手順を実行するスクリプトを実行します。

1. ビルド コマンドから Polyspace オプションを抽出します。

   たとえば、makefile を使用してソース コードをビルドする場合、makefile から解析オプションを抽出できます。以下のコマンドは、まず make を実行し、実行されたプロセスから解析オプションを判別します。

   polyspace-configure -output-options-file compile_opts make

   参考:

   • polyspace-configure

   • ビルド コマンド (Makefile) からの Polyspace 解析構成の作成

2. 前に作成したオプション ファイルを使用して解析を実行します。解析に必要な残りのオプションが含まれた 2 番目のオプション ファイルを追加します。

   polyspace-code-prover-server -options-file compile_opts -options-file run_opts

   複数のオプション ファイルの指定を参照してください。

3. 結果を Polyspace Access にアップロードします。

   polyspace-access <login> -upload <resultsFolder> -project <projName> -parent-project <parentProjName>

   ここで、login は、Polyspace Access をホストしている Web サーバーと通信するために必要なオプションの組み合わせです。

   -host <hostName> -port <portNumber> -login <username> -encrypted-password <pwd>

   resultsFolder は、Polyspace の結果を含むフォルダーです。projName と parentProjName は、Polyspace Access Web インターフェイスに表示されるプロジェクト名と親フォルダー名です。

4. 必要に応じて、コード送信の新しい結果を含む電子メール通知を開発者に送信します。電子メールには、添付ファイルと Polyspace Access Web インターフェイスでの結果へのリンクが含まれます。

   Polyspace Code Prover Server の結果を含む電子メール通知の送信を参照してください。

これらの手順を実行するスクリプトの例については、Jenkins を使用した Polyspace 解析のサンプル スクリプトを参照してください。

参考

polyspace-code-prover-server

トピック

• Manage Polyspace Access Results and Users at the Command Line (Polyspace Access)
• Polyspace Code Prover Server の結果を含む電子メール通知の送信
• デスクトップからローカルでホストされているサーバーへの Code Prover 解析の送信
• すべての Polyspace Code Prover 解析オプションのリスト