Polyspace Platform ユーザー インターフェイスでの Code Prover 解析

Polyspace® Platform ユーザー インターフェイスでの C/C++ コードの欠陥のチェック

Polyspace Platform は、Polyspace 製品での C/C++ コードの静的解析と動的テストをサポートする統合環境です。Polyspace Platform ユーザー インターフェイスでは、プロジェクトの作成、ソース ファイルの追加、解析オプションの構成、Code Prover 解析の実行が可能です。

Polyspace オプション

すべて展開する

基本情報

名前See name of Polyspace Platform project (R2024a 以降)
作成者Specify author name for Polyspace Platform project (R2024a 以降)
作成日See date and time when Polyspace Platform project was created (R2024a 以降)
最終更新日時See date and time when Polyspace Platform project was last modified (R2024a 以降)
ソース コードのエンコード (-sources-encoding)ソース ファイルのエンコードを指定する

ソース、インクルード、およびテスト

インクルード パスSpecify paths to folders containing include files (R2023b 以降)
アプリケーション ソース フォルダーAdd source folders to Polyspace Platform project (R2024a 以降)
アプリケーション ソース ファイルAdd source files to Polyspace Platform project (R2024a 以降)

ファイルの包含と除外

ファイル名パターンを含めるSpecify patterns for file names to be included in Polyspace Platform project (R2024a 以降)
パスを除外するSpecify folders or files to be excluded from static analysis or testing (R2024a 以降)

環境変数

プロジェクト変数Define environment variables for use as shorthands in Polyspace Platform project (R2024a 以降)

ターゲットおよびコンパイラ

ソース コードの言語 (-lang)ソース ファイルの言語の指定
C 標準バージョン (-c-version)ソース コードで準拠する C 言語規格を指定
C++ 標準バージョン (-cpp-version)ソース コードで準拠する C++ 言語規格を指定
プロセッサSelect the processor for the current build configuration
コンパイル ツールチェーン (静的解析)静的解析用のソース コードのビルドに使用するコンパイラを指定します。
負の整数除算結果の負方向への丸め (-div-round-down)コンパイラが、2 つの整数の除算による負の商を負方向に丸めるよう指定します (R2023b 以降)
パック アライメント値 (-pack-alignment-value)Visual C++ で開発したコードの既定の構造体パック アライメントの指定
算術シフトとして符号付き整数を右にシフト (-logical-signed-right-shift)コンパイラが符号付き整数の右シフトを算術シフトとして実装するよう指定する (R2023b 以降)
プリプロセッサ定義 (-D)前処理済みのコード内でのマクロの置き換え
無効なプリプロセッサ定義 (-U)前処理済みのコード内でのマクロの定義解除
強制インクルード (-include)どのソース ファイルでも #include されるファイルを指定します。 (R2023b 以降)
追加のインクルード パス (-I)Specify build-specific include paths in addition to project-wide include paths (R2024a 以降)

環境設定

ファイルがコンパイルされない場合は解析を停止 (-stop-if-compile-error)コンパイル エラーによって解析を停止しなければならないことを指定
前処理済みファイルに適用するコマンド/スクリプト (-post-preprocessing-command)解析の前処理段階の後で、ソース ファイルに対して実行するコマンドまたはスクリプトを指定
DOS または Windows ファイル システムからのコード (-dos)ファイル パスが MS-DOS スタイルであることの考慮

入力およびスタブ

制約の設定 (-data-range-specifications)グローバル変数、関数の入力およびスタブ関数の戻り値の制約
グローバル変数の既定の初期化を無視する (-no-def-init-glob)グローバル変数がコード内で明示的に初期化されていない場合、未初期化と見なす
スタブを生成する関数 (-functions-to-stub)解析時にスタブ化する関数の指定
使用するライブラリ (-library)プログラムで使用するライブラリの指定 (R2021a 以降)

マルチタスキング

Code Prover の同時実行の自動検出を有効にする (-enable-concurrency-detection)マルチスレッド関数の特定ファミリの自動検出
ファイルを使用してマルチタスキング構成を指定外部ファイルを使用してマルチタスキング構成を設定するかどうかの指定 (R2023b 以降)
マルチタスキング用の外部ファイルマルチタスキング構成の設定に使用する、サポートされている外部ファイル形式を指定します。 (R2023b 以降)
マルチタスクを手動で構成コードがマルチタスキングを対象としていることの考慮
タスク (-entry-points)マルチタスク アプリケーションのタスクとして機能する関数の指定
周期タスク (-cyclic-tasks)周期タスクを表す関数の指定
割り込み (-interrupts)非プリエンプタブル割り込みを表す関数の指定
クリティカル セクション詳細 (-critical-section-begin -critical-section-end)クリティカル セクションを開始、終了する関数の指定
時間的に排他なタスク (-temporal-exclusions-file)同時に実行できないエントリ ポイント関数の指定

実行時エラー

アプリケーション全体の検証ソース ファイルが不完全で main 関数が含まれていない場合に検証を停止
グローバル変数の共有と使用のみを表示 (-shared-variables-mode)グローバル変数の共有と使用を完全解析を実行することなく計算
コードの初期化セクションのみの検証 (-init-only-mode)初期化コードのみのランタイム エラーとその他の問題のチェック
モジュールまたはライブラリの検証 (-main-generator)main を含まないモジュールまたはライブラリがソース ファイルである場合に関数 main を生成
クラス (-class-analyzer)検証するクラスの指定
指定クラス内で呼び出す関数 (-class-analyzer-calls)検証するクラス メソッドの指定
クラスの内容のみを解析 (-class-only)クラス メソッド以外のコードを解析しない
メンバー初期化チェックをスキップ (-no-constructors-init-check)クラス コンストラクターがクラス メンバーを初期化するかどうかをチェックしない
初期化する変数 (-main-generator-writes-variables)生成された main により初期化するグローバル変数の指定
初期化関数 (-functions-called-before-main)生成された main により他の関数より先に呼び出す関数の指定
呼び出す関数 (-main-generator-calls)生成された main により初期化関数の後に呼び出す関数の指定

検証の前提条件

浮動小数点の丸めモード (-float-rounding-mode)浮動小数点演算の結果を判定する際に考慮する丸めモードの指定
フィールドに volatile 修飾子があることを考慮する (-consider-volatile-qualifier-on-fields)コード内のどの位置にあっても、構造体の volatile 修飾子付きフィールドは取り得るすべての値を含む可能性があると仮定
環境ポインターが安全でないことを考慮する (-stubbed-pointers-are-unsafe)制約を設けない限り、環境ポインターはデリファレンスに対して安全でない可能性があることを指定
アセンブリ コードを無視 (-ignore-assembly-code)Specify that assembly instructions in C/C++ code cannot modify C/C++ variables (R2023a 以降)

チェック動作

左シフトで負のオペランドを許可 (-allow-negative-operand-in-shift)負の数値での左シフト演算の許可
符号付き整数のオーバーフロー モード (-signed-integer-overflows)オーバーフローの結果をラップするか切り捨てるかを指定
符号なし整数のオーバーフロー モード (-unsigned-integer-overflows)オーバーフローの結果をラップするか切り捨てるかを指定
非有限の浮動小数点を検討 (-allow-non-finite-floats)無限大と NaN を組み込んだ解析モードの有効化
無限大 (-check-infinite)結果が無限大になる浮動小数点演算の処理方法の指定
NaN (-check-nan)結果が NaN になる浮動小数点演算の処理方法の指定
非正規検出モード (-check-subnormal)非正規浮動小数点値になる演算の検出
未初期化のチェックを無効にする (-disable-initialization-checks)未初期化変数および未初期化ポインターのチェックの無効化
スコープ外のスタック ポインター デリファレンスを検出 (-detect-pointer-escape)関数がそれ自体のローカル変数の 1 つを指すポインターを返すケースを検索
構造体の不完全または部分的割り当てを許可する (-size-in-bytes)メモリ バッファーが十分でないポインターが構造体を指すことを許可
呼び出されない関数の検出 (-uncalled-function-checks)main 関数または別のエントリ ポイント関数から直接または間接的に呼び出されない関数の検出
影響の解析を有効化 (-impact-analysis)Check for presence or absence of impact between program elements designated as sources and sinks (R2023b 以降)
ソースとシンクの指定 (-impact-specifications)Specify XML file that identifies program elements as sources and sinks for impact analysis (R2023b 以降)
影響の解析の結果のみを表示 (-impact-analysis-only)Skip regular Code Prover checks for run-time errors and perform impact analysis only (R2023b 以降)
スタック使用量の計算 (-stack-usage)スタック使用量の推定値の計算と表示 (R2022a 以降)

精度

精度レベル (-O0 | -O1 | -O2 | -O3)検証の精度レベルの指定
検証レベル (-to)コードに対する検証プロセスの実行回数の指定
状況依存性 (-context-sensitivity)エラーの原因となった関数呼び出しを識別する呼び出しコンテキスト情報の保存
手続き間解析の精度を高める (-path-sensitivity-delta)行数が少ないコードに対する特定の検証の近似の回避
特定の精度 (-modules-precision)残りの検証よりも高い精度で検証するソース ファイルの指定

スケーリング

インライン (-inline)関数呼び出しのたびに内部でクローンを作成しなければならない関数を指定
構造体内の検証の深さの設定構造体内の検証の深さを設定することを指定する (R2023b 以降)
構造体内の検証の深さ (-k-limiting)入れ子構造体の解析の深さの制限

レポート

レポートの生成解析後にレポートを生成するかどうかの指定
レポート テンプレート (Code Prover または Bug Finder)解析レポートを生成するためのテンプレートの指定
出力形式 (-report-output-format)生成されるレポートの出力形式の指定

コンピューティングの設定

検証時間の制限 (-timeout)解析の時間制限の指定

詳細設定

コード検証の終了後に適用するコマンド/スクリプト (-post-analysis-command)解析後に実行されるコマンドまたはスクリプトの指定
その他静的解析用に追加のコマンド ライン フラグを指定する

システム コマンド

polyspace-project -diff, polyspace-project -merge(System Command) Compare and merge Polyspace Platform projects before submission to source control
polyspace-project -convert-psprj-to-workspace(System Command) Convert Polyspace project file to Polyspace Platform workspace file and project files
polyspace-project -generate-launching-script-for(System Command) Generate files needed to run static analysis on a Polyspace Platform project

トピック

入門

プロジェクトの作成と更新

プロジェクトの構成

Polyspace Platform ユーザー インターフェイス

ファイル ストレージ