オーバーフロー チェックのレビューと修正

このトピックでは、Polyspace^® Code Prover™ で [オーバーフロー] チェックの結果を体系的にレビューする方法を説明します。

[オーバーフロー] チェックの修正を判断するまでこれらの手順の 1 つ以上に従います。このチェックを修正する方法は複数あります。チェックおよびコードの例については、オーバーフローを参照してください。

特にオレンジ チェックに対して、チェックが実際のエラーを表すのではなく、コードに該当しない Polyspace 前提条件を表していると判定できます。前提条件を緩和するのに解析オプションを使用できる場合、そのオプションを使用して検証を再実行します。それ以外の場合は、結果またはコードにコメントおよび正当化情報を追加できます。

すべてのチェックに適用される一般的なワークフローについては、Interpret Polyspace Code Prover Results in Polyspace Platform User InterfaceまたはPolyspace Access Web インターフェイスでの Code Prover の結果の解釈 (Polyspace Access)を参照してください。

チェック情報の解釈

[結果の詳細] でチェックを確認します。

ツールヒントから次の情報を取得します。

• オーバーフローを回避するために制約可能なオペランド変数。

  前述の例では、左側のオペランドには全範囲の値が含まれています。

  考えられる解決方法: オーバーフローを回避するには、演算子が特定の範囲にある場合にのみ演算を実行します。たとえば、このコードは val を 2 で乗算する前に、これが INT_MAX/2 よりも小さいかどうかを確認します。

  if(val < INT_MAX/2)
      return(val*2);
  else 
      /* Alternate action */

• オーバーフローについて考えられる根本原因 — チェックのツールヒントに、考えられる原因が示される場合があります。

  

  前述の例では、スタブ関数 random_int が考えられる原因として識別されています。

  考えられる解決方法: オーバーフローを回避するには、random_int の戻り値を制約します。たとえば、random_int が 1..10 などの特定の範囲内で値を返すよう指定します。詳細については、スタブ関数に関する Code Prover の仮定を参照してください。

チェックの根本原因の判定

制約するオペランド変数から開始してデータ フローをトレースします。制約を指定するのに適したポイントを特定します。

次の例では、tempVal から開始してデータ フローをトレースします。

val = func();
.
.
tempVal = val;
.
.
tempVal++ ;

この例では、以下のような場合があります。

1. tempVal は val から全範囲の値を取得しています。

   考えられる解決方法: val が特定の値未満である場合のみ、val を tempVal に割り当てます。

2. val は func から全範囲の値を取得しています。

   考えられる解決方法: func がスタブされている場合、func の戻り値を func の本体内または Polyspace の [制約指定] インターフェイスで制約します。詳細については、スタブ関数に関する Code Prover の仮定を参照してください。

データ フローをトレースするには、チェックを選択し、[結果の詳細] ペインの情報を確認します。

• [結果の詳細] ペインでチェックにつながる命令の順序が表示される場合、各命令を選択します。

• [結果の詳細] ペインに、そのチェックの考えられる原因の行番号が表示される場合、[ソース] ペインを右クリックします。[行に移動] を選択します。

• そうしない場合は、次のようになります。

  1. オペランド変数の前の書き込み操作を検索します。

     例: tempVal の前の書き込み操作は tempVal=val です。

  2. 前の書き込み操作で、逆にトレースするために新しい変数を特定します。

     書き込み操作に含まれる変数の上にカーソルを置き、その値を確認します。これらの値は、トレースする変数を判断する際に役立ちます。

     例: tempVal=val では、val は全範囲の値を取ることがわかります。したがって、val をトレースします。

  3. 新しい変数の前の書き込み操作を検索します。制約を指定するポイントを特定するまでこの方法で逆にトレースを続行します。

     例: val の前の書き込み操作は val=func() です。func の戻り値に対する制約を指定するように選択できます。

変数に応じて、以下のナビゲーション ショートカットを使用し、前のインスタンスを検索します。以下の手順は、Polyspace Platform ユーザー インターフェイスで実行できます。

変数	変数の前のインスタンスの検索方法
ローカル変数	次のいずれかの方法を使用してください。 変数の検索。 変数を右クリックします。[すべての参照を検索] を選択します。 変数のすべてのインスタンスは、現在のインスタンスが強調表示されて [検索] ペインに表示されます。 [検索] ペインで前のインスタンスを選択します。 ソース コードの参照。 [ソース] ペインで変数をダブルクリックします。 変数のすべてのインスタンスは強調表示されます。 上にスクロールして前のインスタンスを検索します。
グローバル変数 変数を右クリックします。オプション [変数アクセス ビューで表示] が表示される場合、変数はグローバル変数です。	オプション [[グローバル変数の使用] を表示] を選択します。 [グローバル変数アクセス] ペインでは、変数の現在のインスタンスが表示されます。 このペインで、変数の前のインスタンスを選択します。 変数の書き込み操作は で示され、読み取り操作は で示されます。
関数の戻り値 ret=func();	関数定義を検索します。 [ソース] ペインの func を右クリックします。オプションが存在する場合、[定義に移動] を選択します。Polyspace で定義を利用できない場合は、オプションを選択すると関数宣言に移動します。 func の定義では、各 return ステートメントを特定します。関数が返す変数が逆にトレースするための新しい変数です。

任意の操作に含まれる変数が前の操作に関連しているかどうかを判断することもできます。コード内の変数間の関係の検出を参照してください。

ヒント

整数オーバーフローと浮動小数点のオーバーフローを区別するには、[結果の詳細] ペインの [詳細] 列を使用します。列ヘッダーをクリックして、整数オーバーフローと浮動小数点のオーバーフローをグループ化します。[詳細] 列が表示されていない場合は、他の列ヘッダーを右クリックして、この列を有効にします。

チェックの一般的な原因の検索

オーバーフローの原因となる演算がループ内または再帰関数の本体内で発生する場合、次の手順に従います。

• ループの実行または再帰の数を減らすことができるか確認します。

• 演算のオーバーフローの前で、ループまたは再帰関数内に終了条件を置けるかどうかを確認します。

Polyspace の前提条件へのチェックをトレース

コードの前方で発生する Polyspace 前提条件にオレンジ チェックをトレースできるかどうかを確認します。前提条件があてはまらない場合、結果またはコードにコメントまたは正当化情報を追加します。バグ修正または正当化による Polyspace の結果への対処またはPolyspace Access でのバグ修正または正当化による結果への対処 (Polyspace Access)を参照してください。

たとえば、コード内で volatile 変数を使用しているとします。ここで、次のようにします。

1. Polyspace は、volatile 変数がコード内の各ステップで全範囲であると仮定します。

2. その変数を使用する演算はオーバーフローする可能性があり、そのため、オレンジになります。

3. 変数が値がより小さな範囲を取るとわかっている場合、コードにコメントおよび正当化情報を追加し、コードを変更しなかった理由を説明します。

詳細については、Code Prover 解析の前提条件を参照してください。

メモ

オレンジ チェックを正当化する前に、コード設計を改善できるかどうかを十分に検討してください。