unchecked_assert

Polyspace 製品での静的解析で変数範囲を制約する

構文

unchecked_assert(condition);

説明

unchecked_assert(condition); は、以降のコードの Polyspace® 解析での変数範囲に対して制約を適用する、関数のような C/C++ マクロです。たとえば以下の例では、Polyspace は return ステートメントを解析する際に、arg には値 0 が含まれないと仮定します。

double reciprocal (int arg) {
      unchecked_assert(arg != 0);
      return 1.0/arg;
}

このマクロは C/C++ 言語規格に含まれていないため、コンパイル エラーを回避するには、次のようなプリプロセッサ命令でマクロを囲む必要があります。

#ifdef POLYSPACE
   unchecked_assert(arg != 0);
#endif
このコードを Polyspace で解析する際は、マクロ POLYSPACE を定義済みプリプロセッサ命令として指定します。たとえば、コマンド ラインで解析オプション -D POLYSPACE を追加します。プリプロセッサ定義 (-D) を参照してください。このようにプリプロセッサ命令で unchecked_assert マクロを囲むと、このマクロが通常のコンパイル時ではなく、Polyspace 解析で表示されるようになります。

unchecked_assert マクロで指定された制約は、解析での仮定の一部になります。解析ではこの制約を仮定しますが、制約が実際に存在するかはチェックしません。制約がチェックされるようにするには、unchecked_assert の代わりに、標準の C デバッグ マクロ assert を使用します。

使用法

[制約の設定] (-data-range-specifications) などの Polyspace 解析オプションでは直接サポートされていない外部制約を適用するには、unchecked_assert マクロを使用します。外部制約を指定する際は、次の点に注意してください。

  • unchecked_assert を使用して、変数に対する前提条件をプログラム境界で指定します。具体的には、次に関する前提条件です。

    • 呼び出されない関数への入力 (main がない場合)

    • 未定義の (スタブ) 関数の戻り値と変更可能なパラメーター

    プログラム フローの途中で制約を挿入する必要がある場合は、unchecked_assert の代わりに、標準の C デバッグ マクロ assert を使用します。Code Prover では、(以降の解析で制約を適用するだけではなく) [ユーザー アサーション] チェックを使用して、制約が実際に適用されているかどうかを判断します。

  • 実際の外部の考慮事項に基づく制約のみを指定する場合は、unchecked_assert を使用します。たとえば、物理量 (温度、効率比など) として物理的にありえない値を排除するための制約を適用できます。

例

呼び出されない関数に対する入力間に関係を適用する

次の例を考えます。

double getCoefficient(int item, int match)
{
    double coefficient = match/(match-item);
    return coefficient;
}

関数 getCoefficient() は、一見無関係な 2 つの入力 (item と match) を取ります。この関数を呼び出し先なしで解析する場合、Code Prover 解析では次の可能性が考慮されます。

  • 2 つの変数が同じ値をもつ可能性。この場合、解析により、/ 演算での潜在的なゼロ除算が示されます。

  • 変数 item および match が反対の符号をもち、それぞれのデータ型で許容される任意に大きい値をもつ可能性。この場合、解析では、- 演算での潜在的なオーバーフローが示されます。

外部要件により、次の情報が既知であるとします。

  • getCoefficient() の 1 番目のパラメーターの値は正の値である。

  • getCoefficient() の 2 番目のパラメーターの値は "1 番目のパラメーターの値より大きい"。

getCoefficient() の先頭に unchecked_assert ステートメントを入力すると、これらの外部要件を適用できます。

double getCoeff(int item, int match)
{
    #ifdef POLYSPACE
            unchecked_assert(item > 0 && match > item);
    #endif
    
    double coefficient = match/(match-item);
    return coefficient;
}
この例の解析で、POLYSPACE マクロを定義して実質的に制約を有効にするオプションを使用すると、解析で上述の 2 つの潜在的エラーは表示されなくなります。このオプションの詳細については、プリプロセッサ定義 (-D) を参照してください。

未定義関数のパラメーター間に関係を適用する

次の例を考えます。

int getAnItem();
void lookup(int item, int *match);

int main(char argc, char* argv[])
{
    int item = getAnItem(), match;
    lookup(item, &match);
    double coefficient = match/(match-item);
    return 0;
}

変数 item および match は、両方とも未定義の関数 getAnItem() および lookup() で初期化されます。未定義の関数はスタブされるため、Code Prover 解析では次の可能性が考慮されます。

  • 2 つの変数が同じ値をもつ可能性。この場合、解析により、/ 演算での潜在的なゼロ除算が示されます。

  • 変数 match および item が反対の符号をもち、それぞれのデータ型で許容される任意に大きい値をもつ可能性。この場合、解析では、- 演算での潜在的なオーバーフローが示されます。

外部要件により、次の情報が既知であるとします。

  • 関数 getAnItem() は正の値を返す。

  • 関数 lookup() は、2 番目の引数のポインター渡しに正の値を書き込む。書き込まれる値は "1 番目の引数の値より大きい"。

関数 getAnItem() および lookup() のダミー定義を入力できます。ダミー定義の中で、unchecked_assert ステートメントを使用して外部要件を適用できます。

int getAnItem();
void lookup(int item, int *match);

#ifdef POLYSPACE

// Function to initialize a variable with a random value
int getRandomValue();

// Dummy definition of getAnItem()
// Function returns a positive value
int getAnItem()
{
    int ret = getRandomValue();
    unchecked_assert(ret > 0);
    return ret;
}

// Dummy definition of lookup()
// Function writes its second argument
// With a positive value greater than first argument
void lookup(int item, int *match)
{
    *match = getRandomValue();
    unchecked_assert(*match > 0 && *match > item);
}
#endif

int main(char argc, char* argv[])
{
    int item = getAnItem(), match;
    lookup(item, &match);
    double coefficient = match/(match-item);
    return 0;
}
この例の解析で、POLYSPACE マクロを定義して実質的にダミー関数定義を有効にするオプションを使用すると、解析で上述の 2 つの潜在的エラーは表示されなくなります。このオプションの詳細については、プリプロセッサ定義 (-D) を参照してください。

バージョン履歴

R2013b で導入

参考