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

たとえば、継続的インテグレーション中にサーバーでスクリプトを使用して定期的に Polyspace^® を実行する場合には、解析がエラーなしで完了するように、すべての解析オプションを事前に設定しておく必要があります。新しいコード送信に対応するため、これらのオプションを必要に応じて更新する必要があります。ビルドコマンド (makefile) などの既存のアーティファクトを使用して新しいコード送信をビルドする場合は、ビルドコマンドを再利用して Polyspace 解析を構成し、新しい送信に対応することができます。polyspace-configure コマンドでは、ビルドコマンドの実行を監視し、Polyspace による解析のためのオプションファイルを作成できます。

このトピックでは、ビルドコマンドからオプションファイルを作成し、このファイルを後続の解析に使用する方法を説明する、簡単なチュートリアルを示します。このトピックでは Linux^® makefile と GCC コンパイラを使用しますが、Windows^® などの他のオペレーティングシステムや、Microsoft^® Visual Studio^® などの他のコンパイラに合わせてコマンドを変更できます。

デモソースファイルを polyspaceserverroot\polyspace\examples\cxx\Bug_Finder_Example\sources から書き込み権限のあるフォルダーにコピーします。ここで、polyspaceserverroot は Polyspace Server 製品のルートインストールフォルダーです。たとえば、C:\Program Files\Polyspace Server\R2019a です。
デモソースファイルをコンパイルするシンプルな makefile を作成します。ソースファイルと同じフォルダーにこの makefile を保存します。
たとえば、makefile という名前のファイルを作成して、次の内容を追加します。
```
CC := gcc
SOURCES := $(wildcard *.c)

all: $(CC) -c $(SOURCES)
```
ソースファイルが makefile によって正常にビルドされたことを確認します。コマンドターミナルを開き、(cd を使用して) そのフォルダーに移動し、以下を入力します。
```
make -B
```
make コマンドはエラーなしで完了するはずです。
-B オプションを使用すると、makefile 内のすべてのターゲットが確実にビルドされます。通常、make などのビルドコマンドは、前回のビルド以降に変更されたソースだけをビルドするようにセットアップされています。しかし、polyspace-configure では、Polyspace プロジェクトまたはオプションファイルに追加するソースを決定するために、フルビルドが必要です。
polyspace-configure でビルドコマンドをトレースして、オプションファイル compile_opts を作成します。
```
polyspace-configure -output-options-file compile_opts make -B
```
追加のオプションを含む 2 番目のオプションファイルを作成します。たとえば、ファイル run_opts を作成して次の内容を追加します。
```
-checkers numerical
-report-template BugFinder
-output-format pdf
```
これらのオプションは、Bug Finder ですべての数値チェッカーを実行し、解析後に BugFinder テンプレートを使用して PDF レポートを作成します。
2 つのオプションファイル (ビルドコマンドから作成される compile_opts と、手動で作成した run_opts) を使用して Bug Finder 解析を実行します。
Polyspace Bug Finder™:
```
polyspace-bug-finder -options-file compile_opts -options-file run_opts
```
Polyspace Bug Finder Server™:
```
polyspace-bug-finder-server -options-file compile_opts -options-file run_opts
```
解析はエラーなしで完了するはずです。結果を Polyspace ユーザーインターフェイスで開くか、または polyspace-access -upload (Polyspace Access) コマンドを使用して Polyspace Access Web インターフェイスに結果をアップロードできます。
Bug Finder ではなく Code Prover を実行するには、polyspace-bug-finder-server コマンドではなく polyspace-code-prover-server コマンドを使用します。

MATLAB スクリプトを使用して同様の解析を実行できます。polyspace-bug-finder を関数 polyspaceBugFinder に置き換え、polyspace-configure を関数 polyspaceConfigure に置き換えます。

参考

polyspace-configure | polyspace-bug-finder-server

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

参考

参考

トピック

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