すべての Polyspace Code Prover 解析オプションのリスト
Polyspace を使用するときには、既定の解析オプションの変更が必要になる場合があります。コンパイルの問題の回避、Code Prover の仮定の修正、チェック動作の変更などの目的でオプションを変更できます。Polyspace デスクトップ製品のユーザー インターフェイスでは、これらのオプションは [コンフィギュレーション] ペインでグループに従って編成されています。
Polyspace デスクトップ ユーザー インターフェイス、Polyspace コマンド ライン インターフェイス、またはオプション ファイルを使用して解析オプションを指定できます。
Polyspace ユーザー インターフェイス: プロジェクト モジュールの解析オプションを変更するには、[プロジェクト ブラウザー] でそのモジュールの [コンフィギュレーション] ノードを選択します。必要に応じて、[コンフィギュレーション] ペインでオプションを変更します。Polyspace デスクトップ ユーザー インターフェイスでの解析の実行を参照してください。
コマンド ライン:Polyspace 解析をコマンド ラインから実行する際に解析オプションを指定するには、
polyspace-code-prover
またはpolyspace-code-prover-server
にオプションを追加します。コマンド ラインからの Polyspace 解析の実行を参照してください。オプション ファイル:オプション ファイルは、1 行につきオプションと値の 1 つのペアが指定されているテキスト ファイルです。複数のオプションを明示的に列挙する代わりに、コマンド ラインでオプション
-options-file
の値としてオプション ファイルを指定できます。Polyspace 解析のオプション ファイルを参照してください。
カテゴリ
- ターゲットおよびコンパイラ
ターゲット環境の指定
- マクロ
前処理用マクロの定義
- 環境設定
コンパイルの制御
- 入力およびスタブ
グローバル変数と関数の範囲の指定
- マルチタスキング
タスク エントリ ポイント、クリティカル セクション、排他的タスク
- コーディング規約およびコード メトリクス
ワークフローを Bug Finder に移行してください。Bug Finder を使用したコーディング ルールのチェック、カスタム ルールの指定、およびコード複雑度メトリクスの生成
- Code Prover 検証
アプリケーションまたはモジュール全体の検証
- 検証の前提条件
ソース コードに関するソフトウェア前提の設定
- チェック動作
実行時チェック既定の動作の変更
- 精度
検証の精度の指定
- スケーリング
検証のスケーリングの指定
- レポート
レポートの生成
- 実行設定
リモート検証の指定
- 詳細設定
事後解析コマンドとその他のオプション
- コマンド ラインのみでのオプション
コマンド ラインでのみ使用可能なオプションの説明