バッファー サイズ計算でのオーバーフローの検出

unsigned 整数からバッファーのサイズを計算する場合、[符号なし整数のオーバーフロー モード] オプションで、既定値 [allow] の代わりに [forbid] を使用します。このオプションを使用すると、バッファー計算段階でのオーバーフロー検出に役立ちます。使用しない場合、後にバッファー不足によるエラーが発生する可能性があります。このオプションは、[構成] ペインの [Code Prover 検証] の下にある [チェック動作] ノードで使用できます。

以下の例では、次のような C コードをファイル display.c に保存します。

#include <stdlib.h>
#include <stdio.h>

int get_value(void);
 
void display(unsigned int num_items) {
 int *array;
 array = (int *) malloc(num_items * sizeof(int)); // overflow error
  if (array) {
    for (unsigned int ctr = 0; ctr < num_items; ctr++)     {       
      array[ctr] = get_value();
    }
    for (unsigned int ctr = 0; ctr < num_items; ctr++)     {       
      printf("Value is %d.\n", ctr, array[ctr]);
    }
    free(array);
  }
}

void main() {
  display(33000);
}

  1. Polyspace® プロジェクトを作成し、display.c をそのプロジェクトに追加します。

  2. [構成] ペインで、次のオプションを選択します。

    • ターゲットおよびコンパイラ: [ターゲット プロセッサ タイプ] ドロップダウン リストで、[c167] など、16 ビットの int を備えた型を選択します。

    • チェック動作: [符号なし整数のオーバーフロー モード] ドロップダウン リストで、[allow] を選択します。

  3. 検証を実行し、結果を開きます。

    Polyspace は、[不適切にデリファレンスされたポインター] のオレンジ エラーを array[ctr] = get_value() の行で検出し、[無限ループ] のレッド エラーを for ループで検出します。

    このエラーは、前のエラーから派生しています。16 ビット int の場合、num_items * sizeof(int) の計算でオーバーフローが生じます。これは unsigned 整数を使った計算で発生するため、Polyspace はそのオーバーフローを検出しません。Polyspace はこの計算結果をラップし、それが原因で、後に [不適切にデリファレンスされたポインター] エラーが発生します。

  4. [符号なし整数のオーバーフロー モード] ドロップダウン リストで、[forbid] を選択します。

  5. Polyspace は、[オーバーフロー] のレッド エラーを num_items * sizeof(int) の計算で検出します。

参考

Polyspace 解析オプション

Polyspace 結果