Code Prover の実行時チェックの順序

同じ演算に対して複数のチェックが実行される場合、Code Prover はそれらを特定の順序で実行します。チェックの順序が重要となるのは、いずれかのチェックがグリーンでない場合のみです。チェックがレッドの場合、その後のチェックは実行されません。チェックがオレンジの場合、その後のチェックは絞り込まれた値のセットに対して実行されます。詳細は、レッド チェックおよびオレンジ チェック以降の Code Prover 解析を参照してください。

簡単な例は、ポインターのデリファレンスに対するチェックの順序です。Code Prover は最初にポインターが初期化されているかどうかをチェックした後、ポインターが有効な場所を指しているかどうかをチェックします。チェック [不適切にデリファレンスされたポインター] は、チェック [未初期化ローカル変数] の後に実行されます。

二項演算のいずれかのオペランドが浮動小数点変数の場合、Code Prover は演算に対しこの順序でチェックを実行します。

  1. 浮動小数点での無効な演算: 非有限の浮動小数点を考慮するオプションを有効にしている場合、このチェックでは、演算結果が NaN になる可能性があるかどうかを判別します。

  2. オーバーフロー: このチェックでは、結果がオーバーフローするかどうかを判別します。

    非有限の浮動小数点を考慮するオプションを有効にしている場合、このチェックでは、演算結果が無限大になる可能性があるかどうかを判別します。

  3. 非正規浮動小数点: 非正規検出モードを有効にしている場合、このチェックでは、演算結果が非正規値になる可能性があるかどうかを判別します。

たとえば、無限大、NaN および非正規の結果を禁止するオプションを有効にしているとします。この例では、演算 y = x + 0; が 3 つすべての問題についてチェックされます。演算はレッドで表示されますが、オレンジの [浮動小数点での無効な演算] チェック、オレンジの [オーバーフロー] チェックおよびレッドの [非正規浮動小数点] チェックの 3 つのチェックで構成されています。

#include <float.h>
#include <assert.h>

double input();

int main() {
  double x = input();
  double y;
  assert (x != x || x > DBL_MAX  || (x > 0. && x < DBL_MIN));
  y = x + 0.;
  return 0;
}

+ 演算において、x は次の 3 つの値グループに入る可能性があります。x が NaN、x > DBL_MAX および x > 0. && x < DBL_MIN です。

チェックは以下の順序で実行されます。

  1. 浮動小数点での無効な演算: 1 つの実行パスで x が NaN になる可能性を考慮するので、チェックはオレンジになります。

    以降のチェックにおいて、このパスは考慮されません。

  2. オーバーフロー: 1 つの実行パス グループが x > DBL_MAX を考慮するので、チェックはオレンジになります。このパス グループでは、+ 演算は無限大になる可能性があります。

    次のチェックにおいて、このパス グループは考慮されません。

  3. 非正規浮動小数点: 残りの実行パス グループでは、x > 0. && x < DBL_MIN。x のすべての値で、結果が非正規になります。そのため、このチェックはレッドになります。

[結果の詳細] ペインのメッセージに、このパスの減少が反映されます。[非正規浮動小数点] チェックに関するメッセージには (when finite) が表示され、無限値が考慮対象から削除されたことが示されます。

左オペランドと右オペランドの値は演算前の値を、絞り込まれた値のセットではなく、すべて反映しています。そのため、Inf と NaN の値がチェックで考慮されなくても、左オペランドにはこれらの値が示されます。

参考

| | | | |

トピック