特定の精度 (-modules-precision)

残りの検証よりも高い精度で検証するソース ファイルの指定

説明

このオプションは Code Prover 解析のみに影響します。

検証全体に対するよりも高い精度レベルで検証するソース ファイルを指定します。

オプションの設定

以下のいずれかの方法を使用してオプションを設定します。

  • Polyspace® ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [精度] ノードを選択してから、このオプションの値を入力します。最初に有効にしなければならない他のオプションについては、依存関係を参照してください。

  • Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [実行時エラー] 、 [精度] ノードを選択してから、このオプションの値を入力します。最初に有効にしなければならない他のオプションについては、依存関係を参照してください。

  • コマンド ラインとオプション ファイル: オプション -modules-precision を使用します。コマンド ライン情報を参照してください。

このオプションを使用する理由

低い解析精度で特定のファイルを検証すると、そのファイルや他の場所で多くのオレンジ チェックが発生する場合、そのファイルの解析精度を高めることができます。

精度を高めると検証時間も長くなります。

設定

既定値: すべてのファイルは、[精度] 、 [精度レベル] で指定した精度で検証されます。

をクリックし、拡張子 .c を除くファイル名とそれに対応する精度レベルを入力します。

依存関係

このオプションは、[ソース コードの言語] (-lang) が [C] または [C-CPP] に設定されている場合にのみ使用できます。

コマンド ライン情報

パラメーター: -modules-precision
値: file:O0 | file:O1 | file:O2 | file:O3
例 (Code Prover): polyspace-code-prover -sources file_name -O1 -modules-precision My_File:O2
例 (Code Prover Server): polyspace-code-prover-server -sources file_name -O1 -modules-precision My_File:O2

参考

トピック