ゼロ除算チェックのレビューと修正

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

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

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

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

手順 1: チェック情報の解釈

[ゼロ除算] エラーの原因となる / または % 演算の上にカーソルを置きます。

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

• 右オペランドの値 (分母)。

  前述の例では、右オペランド val の範囲にはゼロが含まれています。

  考えられる解決方法: ゼロ除算を回避するには、val がゼロでない場合のみ除算を実行します。

  整数	浮動小数点
  if(val != 0) func(1.0/val); else /* Error handling */	#define eps 0.0000001 . . if(val < -eps || val > eps) func(1.0/val); else /* Error handling */

• ゼロ除算について考えられる根本原因 (ツールヒントに示されている場合)。

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

  考えられる解決方法: ゼロ除算を回避するには、getVal の戻り値を制約します。たとえば、getVal が 1..10 などの特定の範囲内で値を返すよう指定します。制約を指定するには、解析オプション [制約の設定] (-data-range-specifications) を使用します。

手順 2: チェックの根本原因の判定

/ または % 演算の前に、分母がゼロであるかをテストします。分母がゼロである場合、適切なエラー処理を行います。

ゼロ分母を想定しない場合のみ、チェックの根本原因を特定します。分母変数から開始するデータ フローをトレースします。ゼロ値を防ぐために制約を指定できるポイントを特定します。

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

void foo() {
	double time = readTime();
	double dist = readDist();
	.
	.
  bar(dist,time);
}

void bar(double arg1, double arg2) {
	double vel;
	vel=arg1/arg2;
}

以下が見つかる場合があります。

1. bar が全範囲の値で呼び出されています。

   考えられる解決方法: 2 番目の引数 time がゼロより大きい場合のみ bar を呼び出します。

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

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

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

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

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

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

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

     例: arg2 の値は、bar の time の値から書き込みが行われています。

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

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

     例: bar(dist,time) では、time は全範囲の値を取ることがわかります。したがって、time をトレースします。

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

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

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

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

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

手順 3: チェックの一般的な原因の検索

[ゼロ除算] チェックの一般的な原因を確認します。

• 非ゼロであることを想定する変数の場合、コード内の変数をテストし、ゼロ値が除外されるかどうかを確認します。

  それ以外の場合は、Polyspace では変数が非ゼロ値であると判断できません。また、コード外部に制約を指定することもできます。Polyspace 解析の外的制約の指定を参照してください。

• 変数にゼロ値が除外されるテストを行う場合、除算のスコープと比較して小さいスコープでテストが発生するかどうかを確認します。

  たとえば、ステートメント assert(var !=0) は if または while ブロック内で発生しますが、var での除算はブロック外部で発生します。コードが if または while ブロックに入らない場合、assert は実行されません。したがって、if または while ブロック外部で Polyspace は var がまだゼロである可能性があると仮定します。

  考えられる解決方法:

  • 小さいスコープでテストが発生する理由について調べます。上記の例では、if または for ブロック外部にステートメント assert(var !=0) を置けるかどうかを確認します。

  • if または while ブロックが常に実行されると想定する場合、実行されないときは調べます。

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

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

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

1. Polyspace は、変数がコード内の各ステップで全範囲を取ると仮定します。この範囲にはゼロも含まれます。

2. 変数による除算は [ゼロ除算] エラーの原因となる場合があります。

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

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

メモ

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

このチェックを無効にする

このチェックは実質的に無効にできます。コンパイラが浮動小数点演算で無限大と NaN をサポートしている場合、無限大と NaN を組み込んだ検証モードを有効にできます。非有限の浮動小数点を検討 (-allow-non-finite-floats)を参照してください。