ターゲット環境とコンパイラの動作の指定
検証の前に、ソース コードの言語 (C または C++)、ターゲット プロセッサ、およびコードのビルドに使うコンパイラを指定します。場合によっては、コンパイラの動作をエミュレートするために、追加のオプションを指定しなければならないことがあります。
検証ではこの指定を使用して、基本型のサイズが判断され、特定のマクロが定義済みと見なされ、コンパイラに合わせて規格が拡張され解釈されます。オプションがランタイム環境に対応していない場合、以下が発生することがあります。
コンパイル エラー
ターゲットに当てはまらない可能性のある検証結果
gmake
などのビルド コマンドを使用してコードをビルドしており、そのビルド コマンドが一定の制限を満たしている場合、コマンド実行後に、そのビルド コマンドからオプションを抽出することができます。そうでない場合は、オプションを明示的に指定します。
ビルド コマンドからのオプションの抽出
ビルド自動化スクリプトを使用してソース コードをビルドする場合、スクリプトから Polyspace® プロジェクトを設定できます。コンパイラに関連付けるオプションは、そのプロジェクトで指定します。
Polyspace デスクトップ製品でビルド コマンドをトレースする方法の詳細は、次を参照してください。
Polyspace ユーザー インターフェイス。ユーザー インターフェイスでの Polyspace の実行を参照してください。
DOS または UNIX® コマンド ライン。
polyspace-configure
を参照してください。MATLAB® コマンド ライン。
polyspaceConfigure
を参照してください。
Polyspace サーバー製品でビルド コマンドをトレースする方法の詳細は、ビルド コマンド (Makefile) からの Polyspace 解析構成の作成を参照してください。
Polyspace プロジェクトを作成する場合、ビルド自動化スクリプト (makefile) は一定の要件を満たしていなければなりません。ビルド システムからのプロジェクト作成の要件を参照してください。
オプションの明示的な指定
ビルド コマンドをトレースできないためにプロジェクトを手動で作成する場合は、オプションを明示的に指定しなければなりません。
Polyspace デスクトップ製品のユーザー インターフェイスで、プロジェクト構成を選択します。[構成] ペインで、[ターゲットおよびコンパイラ] を選択します。オプションを設定します。
DOS または UNIX コマンド ラインでは、
polyspace-bug-finder
、polyspace-code-prover
、polyspace-bug-finder-server
、またはpolyspace-code-prover-server
コマンドにフラグを指定します。MATLAB コマンド ラインでは、関数
polyspaceBugFinder
、polyspaceCodeProver
、polyspaceBugFinderServer
、またはpolyspaceCodeProverServer
に引数を指定します。
オプションは、以下の順序で指定します。
必要オプション:
ソース コードの言語 (-lang)
: すべてのファイルが同じ拡張子 (.c
や.cpp
) の場合、検証ではその拡張子を使用してソース コードの言語が判断されます。そうでない場合は、オプションを明示的に指定します。コンパイラ (-compiler)
: ソース コードのビルドに使用するコンパイラを選択します。コンパイラが見つからない場合は、お使いのコンパイラに近いオプションを使用します。ターゲット プロセッサ タイプ (-target)
コードを実行する予定のターゲット プロセッサを指定します。一部のプロセッサでは、既定の指定を変更することができます。たとえば、プロセッサhc08
の場合、double
型とlong double
型のサイズを 32 ビットから 64 ビットに変更することができます。ターゲット プロセッサが見つからない場合は、独自のターゲットを作成して、基本型のサイズ、
char
の既定の符号属性、ターゲット マシンのエンディアンを指定することができます。汎用ターゲット オプション
を参照してください。
言語固有のオプション:
C 標準バージョン (-c-version)
既定の C 言語規格は、コンパイラの指定によって異なります。明示的にコンパイラを指定しない場合、既定の解析では C99 規格が使用されます。C90 のような以前の規格か、C11 のようなより新しい規格を指定します。C++ 標準バージョン (-cpp-version)
: 既定の C++ 言語規格は、コンパイラの指定によって異なります。明示的にコンパイラを指定しない場合、既定の解析では C++03 規格が使用されます。C++11 や C++14 など、より新しい規格を指定します。
コンパイラ固有のオプション:
このオプションを使用できるかどうかは、
コンパイラ (-compiler)
の指定によって異なります。たとえば、visual
コンパイラを選択する場合、オプション[パック アライメント値] (-pack-alignment-value)
を使用できます。このオプションを使用して、Visual Studio® で使用するコンパイラ オプション/Zp
をエミュレートします。コンパイラ固有のすべてのオプションについては、ターゲットおよびコンパイラを参照してください。
詳細オプション:
このオプションを使用して、検証結果を変更できます。たとえば、オプション
[除算での負方向への丸め] (-div-round-down)
を使用する場合、検証では負の数値の除算の商またはモジュラスは切り捨てると見なされます。コードのコンパイル時に同様のオプションを使用する場合のみ、これらのオプションを使用します。すべての詳細オプションについては、ターゲットおよびコンパイラを参照してください。
コンパイラのヘッダー ファイル:
[diab]
、[tasking]
、または[greenhills]
コンパイラを指定する場合、コンパイラのヘッダー ファイルのパスを指定しなければなりません。Polyspace 解析への標準ライブラリ ヘッダーの指定を参照してください。
それでも解析の実行後にコンパイル エラーが発生する場合は、他のオプションを指定しなければならない場合があります。
マクロの定義: 解析でマクロが未定義と見なされるために、コンパイル エラーが発生する場合があります。これらのマクロを明示的に定義します。
プリプロセッサ定義 (-D)
を参照してください。インクルード ファイルの指定: コンパイラが Polyspace とは異なる標準ライブラリ関数を定義し、コンパイラのインクルード ファイルを指定していないために、コンパイル エラーが発生する場合があります。コンパイラのインクルード ファイルへのパスを明示的に指定します。Polyspace 解析への標準ライブラリ ヘッダーの指定を参照してください。
参考
ソース コードの言語 (-lang)
| コンパイラ (-compiler)
| ターゲット プロセッサ タイプ (-target)
| C 標準バージョン (-c-version)
| C++ 標準バージョン (-cpp-version)
| プリプロセッサ定義 (-D)