制約の設定 (-data-range-specifications)

グローバル変数、関数の入力およびスタブ関数の戻り値の制約

このページをすべて展開する

説明

グローバル変数、関数入力およびスタブ関数の戻り値の制約 (データ範囲指定または DRS とも呼ばれます) を、[制約指定] テンプレート ファイルを使用して指定します。このテンプレート ファイルは、Polyspace® ユーザー インターフェイスで生成できる XML ファイルです。

オプションの設定

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

  • Polyspace ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [入力およびスタブ] ノードを選択してから、このオプションを使用して制約ファイルを作成します。

  • Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [入力およびスタブ] ノードを選択してから、このオプションを使用して制約ファイルを作成します。

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

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

このオプションは、値が実行時にのみ既知であるコード内の、特定のオブジェクトを制約するために使用します。たとえば、ユーザー入力やセンサー値などのオブジェクトです。適切に制約されたオブジェクトを使用すると、Polyspace 結果内の誤検知やオレンジ チェックが減少する可能性があります。

ソース コードに基づいて、Polyspace は、変数の範囲やポインターに許容されるバッファー サイズなどの項目について仮定を行います。仮定は予想よりも幅広くなる場合があります。その理由は次のとおりです。

  • 完全なコードが提供されていない。たとえば、関数定義の一部が提供されなかった場合。

  • 変数に関する一部の情報が実行時にのみ利用可能である。たとえば、コード内の一部の変数が実行時にユーザーから値を取得する場合。

たとえば、現実世界の速度を表す int 変数の場合、その値が 0 より小さくなったり、光の速度より大きくなったりすることはありません。Polyspace は、変数の範囲が [-2^32... 2^32-1] であると仮定します。このように仮定の幅が広いため、以下のようになります。

  • Code Prover では実行時に発生するパスよりも多くの実行パスを考慮する可能性があります。実行パスの 1 つで操作が失敗すると、Polyspace はこの操作に対してオレンジ チェックを付けます。その実行パスが実行時に発生しない場合、オレンジ チェックは誤検知を示します。

  • Bug Finder では誤検知が生じることがあります。

こうした誤検知の数を減らすには、グローバル変数、関数入力、およびスタブ関数の戻り値に適用可能な制約を指定します。

制約を指定したら、それらを以降の解析で使用するために XML ファイルとして保存します。ソース コードを変更したら、以前の制約を更新します。新しい制約テンプレートを作成する必要はありません。

設定

既定値なし

テンプレート ファイルへの絶対パスを入力します。あるいは、 をクリックして制約指定ウィザードを開きます。このウィザードを使用すると、テンプレート ファイルを生成したり既存のテンプレート ファイルへ移動したりできます。

詳細については、Polyspace 解析の外的制約の指定を参照してください。

コマンド ライン情報

パラメーター: -data-range-specifications
値: file
既定値なし
例 (Bug Finder): polyspace-bug-finder -sources file_name -data-range-specifications "C:\DRS\range.xml"
例 (Code Prover): polyspace-code-prover -sources file_name -data-range-specifications "C:\DRS\range.xml"
例 (Bug Finder Server): polyspace-bug-finder-server -sources file_name -data-range-specifications "C:\DRS\range.xml"
例 (Code Prover Server): polyspace-code-prover-server -sources file_name -data-range-specifications "C:\DRS\range.xml"

制約ファイルの絶対パスの指定、または polyspace-bug-finder または polyspace-code-prover コマンドを実行する場所からの相対パスの指定が可能です。

例

すべて展開する

このコードでは、tmp の定義内の乗算演算にオレンジ オーバーフロー チェックが含まれています。Polyspace は関数 getSpeed() の戻り値の範囲が -2^32... 2^32-1 であると仮定しているため、このチェックが表示されます。

//file1.c
extern int getSpeed(); //Returns the reading of speedometer
int main(){
	//...
	int tmp = 2* getSpeed();
	//...
	return 0;
}

このオレンジ チェックを解決するには、getSpeed() の戻り値を [0..30000000] の範囲に制約します。次の制約を含む XML ファイル drs.xml を作成します。

<?xml version="1.0" encoding="UTF-8"?>
<!--EDRS Version 2.0-->
<global>
	<file name="C:\\Users\\example.c">
		<function name="getSpeed"
				  line="1"
				  attributes="extern"
				  main_generator_called="disabled"
				  comment="">
			<scalar name="return"
					line="1"
					base_type="int32"
					complete_type="int32"
					init_mode="PERMANENT"
					init_modes_allowed="4"
					init_range="0  30000000"
					global_assert="unsupported"
					assert_range="unsupported"
					comment=""/>
		</function>
	</file>
</global>

データの範囲を指定したら、再度、検証を実行します。次のコマンドを使用します。

polyspace-code-prover file1.c -data-range-specifications drs.xml -lang c
オレンジ チェックがグリーン チェックに置き換えられます。
extern int getSpeed(); //Returns the reading of speedometer
int main(){
	//...
	int tmp = 2* getSpeed();
	//...
	return 0;
}

参考

|

トピック