データ型からの変数範囲に関する Code Prover の仮定

Polyspace® では、変数の値をコードから判定できない場合、その変数が型で許容される全範囲の値を取ると仮定します。

たとえば、整数型の変数の場合、Polyspace は許容される最小値と最大値を判別するために以下の条件を使用します。

  • C 規格では符号付き n ビットの整数型変数の範囲を少なくとも [-(2n-1-1), 2n-1-1] として指定します。

    [ターゲット プロセッサ タイプ] の指定により特定の型に割り当てられるビット数が決定されます。詳細については、ターゲット プロセッサ タイプ (-target)を参照してください。

  • Polyspace はターゲットが符号付き整数に対して 2 の補数表現を使用すると仮定します。ソフトウェアは変数の正確な範囲を判別するためにこの表現を使用します。この表現では、符号付き n ビットの整数型変数の範囲は [-2n-1, 2n-1-1] です。

たとえば、[i386] プロセッサでは、

  • char 変数は 8 ビットです。C 規格では char 変数の範囲を少なくとも [-127,127] と指定します。

  • 2 の補数表現を使用して、Polyspace は char 変数の正確な範囲を [-128,127] と仮定します。

Polyspace が特定の型に対して仮定する範囲を判別するには、以下を行います。

  1. 次のコードの検証を実行します。type を int のような型名で置き換えます。

    type getVal(void);
void main() {
		type val = getVal();
}

  2. 検証結果を開きます。[ソース] ペインで、カーソルを val に置きます。

    ツールヒントに Polyspace が type に対して仮定した範囲が表示されます。getVal が定義されていないため、Polyspace は getVal の戻り値が type で許容される全範囲の値を取ると仮定します。

参考

トピック