Polyspace Platform ユーザー インターフェイスでの Polyspace Code Prover のオプション
Polyspace Platform ユーザー インターフェイスでは、C/C++ コードに対して次の静的解析を実行できます。
Polyspace® Bug Finder™ を使用して、C/C++ コードで欠陥とコーディング規約違反の有無をチェックできます。
Polyspace Code Prover™ を使用して、C/C++ コードに特定のタイプのランタイム エラーが存在しないことを証明できます。
詳細については、Run Static Analysis in Polyspace Platform User Interfaceを参照してください。
Polyspace Bug Finder または Polyspace Code Prover の解析を実行するために使用するオプションをカスタマイズできます。このトピックでは、Polyspace Platform ユーザー インターフェイスで使用できる Code Prover 解析のオプションについて説明します。
オプションを構成するには、Polyspace Platform プロジェクトの [構成] ノードをダブルクリックします。[構成] ペインでの Code Prover 解析のオプションは、次の 2 つのタブに分けられています。
プロジェクト
次の表に、[プロジェクト] タブにある、Polyspace Code Prover 解析に関連するオプションを記載します。
| オプション | 説明 | 詳細 |
|---|---|---|
| 名前 | Polyspace Platform プロジェクトの名前を表示します。 | 名前 (Polyspace Code Prover)を参照してください。 |
| 作成者 | Polyspace Platform プロジェクトの作成者名を指定します。 | 作成者 (Polyspace Code Prover)を参照してください。 |
| 作成日 | Polyspace Platform プロジェクトが作成された日付と時刻を表示します。 | 作成日 (Polyspace Code Prover)を参照してください。 |
| 最終更新日時 | Polyspace Platform プロジェクトが最後に更新された日付と時刻を表示します。 | 最終更新日時 (Polyspace Code Prover)を参照してください。 |
| ソース コードのエンコード | ソース ファイルのエンコードを指定します。 | ソース コードのエンコード (-sources-encoding) (Polyspace Code Prover) を参照してください。 |
| アプリケーション ソース ファイル | Polyspace Platform プロジェクトにソース ファイルを追加します。 | アプリケーション ソース ファイル (Polyspace Code Prover)を参照してください。 |
| アプリケーション ソース フォルダー | Polyspace Platform プロジェクトにソース フォルダーを追加します。 | アプリケーション ソース フォルダー (Polyspace Code Prover)を参照してください。 |
| インクルード パス | インクルード ファイルが格納されているフォルダーへのパスを指定します。 |
|
| ファイル名パターンを含める | Polyspace Platform プロジェクトに含めるファイルのファイル名パターンを指定します。 | ファイル名パターンを含める (Polyspace Code Prover)を参照してください。 |
| パスを除外する | 静的解析から除外するフォルダーまたはファイルを指定します。 | パスを除外する (Polyspace Code Prover)を参照してください。 |
| プロジェクト変数 | Polyspace Platform プロジェクトで省略形として使用する環境変数を定義します。 | プロジェクト変数 (Polyspace Code Prover)を参照してください。 |
ビルド
[一般] タブにある [ターゲットおよびコンパイラ] ノードは、標準の Polyspace 構成 (つまり、標準の Polyspace ユーザー インターフェイスで作成されたもの) の [ターゲットおよびコンパイラ] ノードと同等ですが、いくつかの小さな相違点があります。相違点の詳細については、Differences in Configuration Options Between Polyspace Projects and Polyspace Platform Projectsを参照してください。
ターゲットおよびコンパイラ
[ターゲットおよびコンパイラ] ノードにあるオプションを以下に記載します。
| オプション | 説明 | 詳細 |
|---|---|---|
| ソース コードの言語 | ソース ファイルの言語の指定 |
|
| C 標準バージョン | ソース コードで準拠する C 言語規格を指定 |
|
| C++ 標準バージョン | ソース コードで準拠する C++ 言語規格を指定 |
|
| プロセッサ | 現在のビルド構成のプロセッサを選択 |
|
| コンパイル ツールチェーン (静的解析) | ソース コードのビルドに使用するコンパイラを指定します。このオプションは静的解析にのみ適用されます。テスト用にコンパイル ツールチェーンを指定するには、オプション [コンパイル ツールチェーン (テスト)] を指定します。 |
|
| 負の整数除算結果の負方向への丸め | コンパイラが、2 つの整数の除算による負の商を負方向に丸めるよう指定します |
|
| パック アライメント値 | Visual C++® で開発したコードの既定の構造体パック アライメントの指定 |
|
| 算術シフトとして符号付き整数を右にシフト | コンパイラが符号付き整数の右シフトを算術シフトとして実装するよう指定する |
|
| プリプロセッサ定義 | 前処理済みのコード内でのマクロの置き換え |
|
| 無効なプリプロセッサ定義 | 前処理済みのコード内でのマクロの定義解除 |
|
| 強制インクルード | どのソース ファイルでも #include されるファイルを指定 |
|
| 追加のインクルード パス | プロジェクト全体のインクルード パスの他に、ビルド固有のインクルード パスを指定 |
|
ビルド コマンドから作成されたプロジェクトでは、次の読み取り専用オプションも参照してください。
暗黙的な C (C++) コンパイラ インクルード パス(Polyspace Code Prover)暗黙的な C (C++) コンパイラ定義(Polyspace Code Prover)
静的解析
[静的解析] タブにあるノードは、標準の Polyspace 構成 (つまり、標準の Polyspace ユーザー インターフェイスで作成されたもの) に含まれる同じ名前を持つノードと同等ですが、いくつかの小さな相違点があります。相違点の詳細については、Differences in Configuration Options Between Polyspace Projects and Polyspace Platform Projectsを参照してください。
環境設定
[環境設定] ノードにあるオプションを以下に記載します。
| オプション | 説明 | 詳細 |
|---|---|---|
| ファイルがコンパイルされない場合は解析を停止 | コンパイル エラーによって解析を停止しなければならないことを指定 |
|
| 前処理済みファイルに適用するコマンド/スクリプト | 解析の前処理段階の後で、ソース ファイルに対して実行するコマンドまたはスクリプトを指定 |
|
| DOS または Windows ファイル システムからのコード | ファイル パスが MS-DOS スタイルであることの考慮 |
|
入力およびスタブ
[入力およびスタブ] ノードにあるオプションを以下に記載します。
| オプション | 説明 | 詳細 |
|---|---|---|
| 制約の設定 | グローバル変数、関数の入力およびスタブ関数の戻り値の制約 |
|
| グローバル変数の既定の初期化を無視する | グローバル変数がコード内で明示的に初期化されていない場合、未初期化と見なす |
|
| スタブを生成する関数 | 解析時にスタブ化する関数の指定 |
|
| 使用するライブラリ | プログラムで使用するライブラリの指定 |
|
マルチタスキング
[マルチタスキング] ノードにあるオプションを以下に記載します。
| オプション | 説明 | 詳細 |
|---|---|---|
| Code Prover の同時実行の自動検出を有効にする | マルチスレッド関数の特定ファミリの自動検出 |
|
| マルチタスキング構成を指定 | 外部ファイルを使用してマルチタスキング構成を設定するかどうかの指定 |
|
| 外部マルチタスキング構成 | マルチタスキング構成の設定に使用する、サポートされている外部ファイル形式を指定します。 |
|
| マルチタスクを手動で構成 | コードがマルチタスキングを対象としていることの考慮 |
|
| タスク | マルチタスク アプリケーションのタスクとして機能する関数の指定 |
|
| 周期タスク | 周期タスクを表す関数の指定 |
|
| 割り込み | 非プリエンプタブル割り込みを表す関数の指定 |
|
| クリティカル セクション詳細 | クリティカル セクションを開始、終了する関数の指定 |
|
| 時間的に排他なタスク | 同時に実行できないエントリ ポイント関数の指定 |
|
実行時エラー
[実行時エラー] ノードにあるオプションを以下に記載します。
| オプション | 説明 | 詳細 |
|---|---|---|
| アプリケーション全体の検証 | ソース ファイルが不完全で main 関数が含まれていない場合に検証を停止 |
|
| グローバル変数の共有と使用のみを表示 | グローバル変数の共有と使用を完全解析を実行することなく計算 |
|
| コードの初期化セクションのみの検証 | 初期化コードのみのランタイム エラーとその他の問題のチェック |
|
| モジュールまたはライブラリの検証 | main を含まないモジュールまたはライブラリがソース ファイルである場合に関数 main を生成 |
|
| クラス | 検証するクラスの指定 |
|
| 指定クラス内で呼び出す関数 | 検証するクラス メソッドの指定 |
|
| クラスの内容のみを解析 | クラス メソッド以外のコードを解析しない |
|
| メンバー初期化チェックをスキップ | クラス コンストラクターがクラス メンバーを初期化するかどうかをチェックしない |
|
| 初期化する変数 | 生成された main により初期化するグローバル変数の指定 |
|
| 初期化関数 | 生成された main により他の関数より先に呼び出す関数の指定 |
|
| 呼び出す関数 | 生成された main により初期化関数の後に呼び出す関数の指定 |
|
検証の前提条件
[検証の前提条件] ノードにあるオプションを以下に記載します。
| オプション | 説明 | 詳細 |
|---|---|---|
| 浮動小数点の丸めモード | 浮動小数点演算の結果を判定する際に考慮する丸めモードの指定 |
|
| フィールドに volatile 修飾子があることを考慮する | コード内のどの位置にあっても、構造体の volatile 修飾子付きフィールドは取り得るすべての値を含む可能性があると仮定 |
|
| 環境ポインターが安全でないことを考慮する | 制約を設けない限り、環境ポインターはデリファレンスに対して安全でない可能性があることを指定 |
|
| アセンブリ コードを無視 | C/C++ コード内のアセンブリ命令では C/C++ 変数を変更できないことを指定 |
|
チェック動作
[チェック動作] ノードにあるオプションを以下に記載します。
| オプション | 説明 | 詳細 |
|---|---|---|
| 左シフトで負のオペランドを許可 | 負の数値での左シフト演算の許可 |
|
| 符号付き整数のオーバーフロー モード | オーバーフローの結果をラップするか切り捨てるかを指定 |
|
| 符号なし整数のオーバーフロー モード | オーバーフローの結果をラップするか切り捨てるかを指定 |
|
| 非有限の浮動小数点を検討 | 無限大と NaN を組み込んだ解析モードの有効化 | 詳細は、 |
| 無限大 | 結果が無限大になる浮動小数点演算の処理方法の指定 |
|
| NaN | 結果が NaN になる浮動小数点演算の処理方法の指定 |
|
| 非正規検出モード | 非正規浮動小数点値になる演算の検出 |
|
| 未初期化のチェックを無効にする | 未初期化変数および未初期化ポインターのチェックの無効化 |
|
| スコープ外のスタック ポインター デリファレンスを検出 | 関数がそれ自体のローカル変数の 1 つを指すポインターを返すケースを検索 |
|
| 構造体の不完全または部分的割り当てを許可する | メモリ バッファーが十分でないポインターが構造体を指すことを許可 |
|
| 呼び出されない関数の検出 | main 関数または別のエントリ ポイント関数から直接または間接的に呼び出されない関数の検出 |
|
| 影響分析を有効化 | ソースとシンクとして指定されているプログラム要素間の影響の有無を確認 |
|
| ソースとシンクの指定 | プログラム要素を影響分析のソースとシンクとして特定している XML ファイルを指定 |
|
| 影響分析の結果のみを表示 | 実行時エラーの通常の Code Prover チェックをスキップして、影響分析のみを実行 |
|
| スタック使用量の計算 | スタック使用量の推定値の計算と表示 |
|
精度
[精度] ノードにあるオプションを以下に記載します。
| オプション | 説明 | 詳細 |
|---|---|---|
| 精度レベル | 検証の精度レベルの指定 |
|
| 検証レベル | コードに対する検証プロセスの実行回数の指定 |
|
| 状況依存性 | エラーの原因となった関数呼び出しを識別する呼び出しコンテキスト情報の保存 |
|
| 手続き間解析の精度を高める | 行数が少ないコードに対する特定の検証の近似の回避 |
|
| 特定の精度 | 残りの検証よりも高い精度で検証するソース ファイルの指定 | 特定の精度 (-modules-precision) (Polyspace Code Prover) を参照してください。 |
スケーリング
[スケーリング] ノードにあるオプションを以下に記載します。
| オプション | 説明 | 詳細 |
|---|---|---|
| インライン | 関数呼び出しのたびに内部でクローンを作成しなければならない関数を指定 |
|
| 構造体内の検証の深さの設定 | 構造体内の検証の深さを設定することを指定する |
|
| 構造体内の検証の深さ | 入れ子構造体の解析の深さの制限 |
|
レポート
[レポート] ノードにあるオプションを以下に記載します。
| オプション | 説明 | 詳細 |
|---|---|---|
| レポートの生成 | 解析後にレポートを生成するかどうかの指定 |
|
| レポート テンプレート (Code Prover) | 解析レポートを生成するためのテンプレートの指定 |
|
| 出力形式 | 生成されるレポートの出力形式の指定 |
|
コンピューティングの設定
[コンピューティングの設定] ノードにあるオプションを以下に記載します。
| オプション | 説明 | 詳細 |
|---|---|---|
| 検証時間の制限 | 検証の時間制限を指定 |
|
詳細設定
[詳細設定] ノードにあるオプションを以下に記載します。
| オプション | 説明 | 詳細 |
|---|---|---|
| コード検証の終了後に適用するコマンド/スクリプト | 検証の時間制限を指定 |
|
| その他 | 解析の追加フラグを指定 |
|
