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

ビルド コマンドを使用した Polyspace 解析のモジュール化

Polyspace^® 解析を設定するために、ビルド コマンドで make などのコンパイル オプションを再利用できます。まず、polyspace-configure (または MATLAB^® の polyspaceConfigure) でビルド コマンドをトレースし、Polyspace オプション ファイルを作成します。このオプション ファイルは、以降の Polyspace 解析に対して後で指定します。

ビルド コマンドで複数のバイナリを作成する場合、既定では polyspace-configure によりすべてのバイナリのソース ファイルが 1 つの Polyspace オプション ファイルにグループ化されます。異なるバイナリに含まれる複数のソース ファイルで同じ関数が使用されている場合、それらを 1 つの解析にまとめると、オプション ファイルの使用時にリンク エラーが発生する可能性があります。特に、main 関数の複数の定義が原因でリンク エラーが発生することがあります。

このトピックでは、makefile で作成されるバイナリごとに個別の Polyspace オプション ファイルを作成する方法を説明します。makefile で、2 つの実行可能ファイル (ターゲット cmd1 および cmd2) と 2 つの共有ライブラリ (ターゲット liba および libb) という 4 つのバイナリが作成されるとします。これらのバイナリごとに個別の Polyspace オプション ファイルを作成することができます。

例のファイル

この例を試すには、polyspaceroot\polyspace\examples\doc_cxx\multiple_modules のファイルを使用します。ここで、polyspaceroot は Polyspace インストール フォルダーです。たとえば、C:\Program Files\Polyspace\R2025a または C:\Program Files\Polyspace Server\R2025a です。

ソース コードのビルド

makefile を検証します。この makefile では次の 4 つのバイナリが作成されます。

CC := gcc

LIBA_SOURCES := $(wildcard src/liba/*.c)
LIBB_SOURCES := $(wildcard src/libb/*.c)
CMD1_SOURCES := $(wildcard src/cmd1/*.c)
CMD2_SOURCES := $(wildcard src/cmd2/*.c)
LIBA_OBJ := $(notdir $(LIBA_SOURCES:.c=.o))
LIBB_OBJ := $(notdir $(LIBB_SOURCES:.c=.o))
CMD1_OBJ := $(notdir $(CMD1_SOURCES:.c=.o))
CMD2_OBJ := $(notdir $(CMD2_SOURCES:.c=.o))
LIBB_SOBJ := libb.so
LIBA_SOBJ := liba.so

all: cmd1 cmd2

cmd1: liba libb
	$(CC) -o  $@ $(CMD1_SOURCES) $(LIBA_SOBJ) $(LIBB_SOBJ)

cmd2: libb
	$(CC) -c $(CMD2_SOURCES) 
	$(CC) -o $@ $(CMD2_OBJ) $(LIBB_SOBJ)

liba: libb
	$(CC) -fPIC -c $(LIBA_SOURCES)
	$(CC) -shared -o $(LIBA_SOBJ) $(LIBA_OBJ) $(LIBB_SOBJ)

libb: 
	$(CC) -fPIC -c $(LIBB_SOURCES)
	$(CC) -shared -o $(LIBB_SOBJ) $(LIBB_OBJ) 

.PHONY: clean
clean: 
	rm *.o *.so

作成されるバイナリには次の図に示す依存関係があります。たとえば、オブジェクト cmd1.o の作成は、フォルダー cmd1 に含まれるすべての .c ファイルと、共有オブジェクト liba.so および libb.so に依存します。

makefile を使用してソース コードをビルドします。フル ビルドが行われるように -B フラグを使用します。

make -B

ビルドの実行が完了したことを確認します。

フル ビルドに対する 1 つの Polyspace オプション ファイルの作成

polyspace-configure を使用してビルド コマンドをトレースします。オプション -output-options-file を使用して、ビルド コマンドから Polyspace オプション ファイル psoptions を作成します。

polyspace-configure -output-options-file psoptions make -B

前に作成したオプション ファイルを使用して Bug Finder または Code Prover を実行します。解析結果を results サブフォルダーに保存します。

polyspace-bug-finder -options-file psoptions -results-dir results

polyspace-code-prover -options-file psoptions -results-dir results

次のリンク エラーが表示されます (Bug Finder での警告)。

Procedure 'main' multiply defined.

エラーが発生するのは、ファイル cmd1/cmd1_main.c および cmd2/cmd2_main.c の両方に main 関数があるためです。ビルド コマンドを実行すると、これら 2 つのファイルがこの makefile の個別のターゲットで使用されます。しかし、既定では polyspace-configure はフル ビルドに対するオプション ファイルを 1 つ作成します。その Polyspace オプション ファイルには両方のソース ファイルが含まれるため、main 関数の定義が競合する結果になります。

エラーの原因を検証するには、Polyspace オプション ファイル psoptions を開きます。競合する main 関数の定義があるファイルを含む次の行が表示されます。

-sources src/cmd1/cmd1_main.c
-sources src/cmd2/cmd2_main.c

ビルド コマンドでの特定バイナリのオプション ファイルの作成

リンク エラーを回避するには、polyspace-configure を使用してビルド コマンドをトレースするときに、特定のバイナリのソース コードをビルドします。

たとえば、バイナリ cmd1.o のソース コードをビルドします。make に対して makefile ターゲット cmd1 を指定すると、このバイナリが作成されます。

polyspace-configure -output-options-file psoptions -allow-overwrite make -B cmd1

前に作成したオプション ファイルを使用して Bug Finder または Code Prover を実行します。

polyspace-bug-finder -options-file psoptions -results-dir results

polyspace-code-prover -options-file psoptions -results-dir results

リンク エラーは発生せずに、解析の実行が完了します。Polyspace オプション ファイル psoptions を開くと、cmd1 サブフォルダーにあるソース ファイルと、共有オブジェクトの作成に関連のあるファイルのみが、-sources オプションに含まれていることを確認できます。バイナリ cmd1.o の作成に関連のない cmd2 サブフォルダーにあるソース ファイルは Polyspace オプション ファイルに含まれていません。

ライブラリの特別な考慮事項 (Code Prover のみ)

ライブラリからの共有オブジェクトの作成をトレースする場合、抽出されるソース ファイルには main 関数が含まれません。以降の Code Prover 解析では、main がないため、エラーが表示される可能性があります。

Polyspace オプション [モジュールまたはライブラリの検証] (Polyspace Code Prover) (-main-generator) を使用して main 関数を生成します。作成したオプション ファイル内か、コマンド ラインで直接このオプションを指定します。main 関数のない C アプリケーションの検証 (Polyspace Code Prover)を参照してください。

C++ では、クラスに次の追加オプションを使用します。

• クラス (-class-analyzer)

• 指定クラス内で呼び出す関数 (-class-analyzer-calls)

ビルド コマンドで作成されるバイナリごとに 1 つのオプション ファイルを作成

ビルド コマンドで作成される特定のバイナリに対してオプション ファイルを作成するには、ビルド コマンドの詳細を知らなければなりません。ビルド コマンドの内部的な詳細を熟知していない場合は、ビルド コマンドで作成される "すべての" バイナリに対し、個別の Polyspace オプション ファイルを作成できます。この方法は、実行可能ファイル、共有 (ダイナミック) ライブラリ、およびスタティック ライブラリであるバイナリに対して有効です。

この方法は以下のリンカーを使用する場合のみ機能します。

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

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

polyspace-configure を使用してビルド コマンドをトレースします。各バイナリに個別のオプション ファイルを作成するには、オプション -module を polyspace-configure で使用します。

polyspace-configure -module -output-options-path optionsFilesFolder make -B

このコマンドはフォルダー optionsFilesFolder にオプション ファイルを作成します。前述の例では、このコマンドは 4 つのバイナリに対して次の 4 つのオプション ファイルを作成します。

• cmd1.psopts

• cmd2.psopts

• liba_so.psopts

• libb_so.psopts

対応するオプション ファイルを使用して、特定のバイナリのコード実装に対して Polyspace を実行できます。たとえば、makefile ターゲット cmd1 から作成されたバイナリのコード実装に対し、次のコマンドを使用して Code Prover を実行できます。

polyspace-bug-finder -options-file optionsFilesFolder\cmd1.psopts -results-dir results

polyspace-code-prover -options-file optionsFilesFolder\cmd1.psopts -results-dir results

polyspace-configure の -module オプションを使用して作成されたすべてのオプション ファイルをループすることも可能です。たとえば、次の Bash スクリプトでは、生成されたすべてのオプション ファイルに対して Polyspace を実行し、そのオプション ファイル名を基に個別の結果フォルダーを作成します。

#!/bin/bash
FILEPATHS=optionsFilesFolder/*.psopts
for filePath in $FILEPATHS
do
    echo "Running Polyspace on $filePath"
    fileName="${filePath##*/}"
    resultsDirName="${fileName%.*}_results"
    logName="${fileName%.*}.log"
    polyspace-bug-finder -options-file "$filePath" -results-dir "${resultsDirName}" >> "${logName}"
done

#!/bin/bash
FILEPATHS=optionsFilesFolder/*.psopts
for filePath in $FILEPATHS
do
    echo "Running Polyspace on $filePath"
    fileName="${filePath##*/}"
    resultsDirName="${fileName%.*}"
    logName="{fileName%.*}.log"
    polyspace-code-prover -options-file "$filePath" -results-dir "${resultsDirName}" >> "${logName}"
done

この方法では、ビルド コマンドの詳細を知っている必要はありません。ただし、この方法でバイナリごとに個別のオプション ファイルを作成する場合、各オプション ファイルには、共有オブジェクトを介したものではなく、バイナリに直接関連するソース ファイルが含まれます。たとえば、この例のオプション ファイル cmd1.psopts では cmd1 サブフォルダーにあるソース ファイルのみが指定され、共有オブジェクト liba.so および libb.so の作成に関連のあるソース ファイルは指定されません。このオプション ファイルを使用する以降の解析では、共有オブジェクトの関数にはアクセスできず、代わりに関数スタブが使用されます。Code Prover 解析で、スタブが原因で非常に多くのオレンジ チェックが表示される場合は、ビルド コマンドでの特定バイナリのオプション ファイルの作成の節に記述された方法を使用します。

ライブラリの特別な考慮事項 (Code Prover のみ)

ライブラリからの共有オブジェクトの作成をトレースする場合、抽出されるソース ファイルには main 関数が含まれません。以降の Code Prover 解析では、main がないため、エラーが表示される可能性があります。

Polyspace オプション [モジュールまたはライブラリの検証] (Polyspace Code Prover) (-main-generator) を使用して main 関数を生成します。作成したオプション ファイル内か、コマンド ラインで直接このオプションを指定します。main 関数のない C アプリケーションの検証 (Polyspace Code Prover)を参照してください。

C++ では、クラスに次の追加オプションを使用します。

• クラス (-class-analyzer)

• 指定クラス内で呼び出す関数 (-class-analyzer-calls)

参考

polyspace-configure | polyspace-bug-finder | polyspace-bug-finder-server

トピック

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