符号なし整数のオーバーフロー モード (-unsigned-integer-overflows)

オーバーフローの結果をラップするか切り捨てるかを指定

説明

このオプションは Code Prover 解析のみに影響します。

Polyspace® で符号なし整数のオーバーフローにフラグを設定するかどうかと、解析でオーバーフローの結果をラップするかまたはその結果を極値に制約するかを指定します。

オプションの設定

以下のいずれかの方法を使用してオプションを設定します。

  • Polyspace ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [チェック動作] ノードを選択してから、このオプションを選択します。

  • Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [実行時エラー] 、 [チェック動作] ノードを選択してから、このオプションを選択します。

  • コマンド ラインとオプション ファイル: オプション -unsigned-integer-overflows を使用します。コマンド ライン情報 (Polyspace Code Prover)を参照してください。

このオプションを使用する理由

Polyspace Code Prover™ による符号なし整数のオーバーフローへの対応方法を指定する場合に、このオプションを使用します。符号なし整数のオーバーフローにフラグを設定し、この問題に続くコードを問題があるものとして扱うように指定します。あるいは、符号なし整数のオーバーフローを許可するように指定します。このオプションの値に応じて、Polyspace が符号なし整数オーバーフローより後のコードを解析する際に用いる仮定が変わります。

設定

既定値: allow

forbid

Polyspace で符号なし整数のオーバーフローにフラグを設定します。演算に対する [オーバーフロー] チェック結果について:

  • レッドの場合、Polyspace は現在のスコープ内で残っているコードを解析しません。

  • オレンジの場合、Polyspace は現在のスコープ内で残っているコードを解析します。Polyspace では以下であると見なします。

    • 正の [オーバーフロー] の後、演算の結果には上限が設けられます。この上限は、結果の型に応じて許可される最大値です。

    • 負の [オーバーフロー] の後、演算の結果には下限が設けられます。この下限は、結果の型に応じて許可される最小値です。

次のコードでは、オレンジのオーバーフロー前に、j は [1..232-1] の範囲内の値をもちます。オーバーフロー後、Polyspace は j が [2 .. 4294967294] の範囲内の偶数値をもつと見なします。レッドのオーバーフロー後、Polyspace は printf() ステートメントを解析しません。

#include<stdio.h>

unsigned int getVal();

void func1()
{
    unsigned int i = 1;
    i = i << 31;
    // Result of * operation overflows
    i = i * 2;
    // Remaining code in current scope not analyzed
    printf("%u", i);
}
void func2()
{

    unsigned int j = getVal();
    if (j > 0) {
        // Range of j: [1..232-1]
        // Result of * operation may overflow
        j = j * 2;
        // Range of j: even values in [2 .. 4294967294]
        printf("%u", j);
    }
}

符号なし整数を使用した演算に関するツールヒントに (result is truncated) と表示され、解析モードであることが示されることに注意してください。このメッセージは、[オーバーフロー] チェックがグリーンの場合も表示されます。

allow

Polyspace は符号なし整数のオーバーフローにフラグを設定しません。演算の結果としてオーバーフローが発生した場合、Polyspace は残りのコードを解析しますが、オーバーフローの結果をラップします。たとえば、MAX_INT + 1 は MIN_INT にラップされます。この動作は、ANSI C (ISO C++) 規格に適合します。

次のコードでは、解析はコード内でのオーバーフローにフラグを設定しません。ただし、j の範囲を範囲 [0..232-2]] の偶数値に、i の値を 0 にそれぞれラップ アラウンドします。

#include<stdio.h>

unsigned int getVal();

void func1()
{
    unsigned int i = 1;
    i = i << 31;
    // i = 231
    i = i * 2;
    // i = 0
    printf("%u", i);
}
void func2()
{

    unsigned int j = getVal();
    if (j > 0) {
        // Range of j: [1..232-1]
        j = j * 2;
        // Range of j: even values in [0 .. 4294967294]
        printf("%u", j);
    }
}

符号なし整数を使用した演算に関するツールヒントに (result is wrapped) と表示され、解析モードであることが示されることに注意してください。このメッセージは、解析で符号なし整数オーバーフローにフラグが設定されない場合も表示されます。

warn-with-wrap-around

Polyspace で符号なし整数のオーバーフローにフラグを設定します。演算の結果としてオーバーフローが発生した場合、Polyspace は残りのコードを解析しますが、オーバーフローの結果をラップします。たとえば、INT_MAX + 1 は 0 にラップされます。

次のコードでは、オレンジのオーバーフロー前に、j は [1..232-1] の範囲内の値をもちます。オーバーフロー後、Polyspace は j が [0 .. 4294967294] の範囲内の偶数値をもつと見なします。

同様に、レッドのオーバーフロー前の i の値は 231 で、レッドのオーバーフロー後の値は 0 になります。

#include<stdio.h>

unsigned int getVal();

void func1()
{
    unsigned int i = 1;
    i = i << 31;
    // i = 231
    i = i * 2;
    // i = 0
    printf("%u", i);
}
void func2()
{

    unsigned int j = getVal();
    if (j > 0) {
        // Range of j: [1..232-1]
        j = j * 2;
        // Range of j: even values in [0 .. 4294967294]
        printf("%u", j);
    }
}

符号なし整数を使用した演算に関するツールヒントに (result is wrapped) と表示され、解析モードであることが示されることに注意してください。このメッセージは、[オーバーフロー] チェックがグリーンの場合も表示されます。

ラップアラウンド モードでは、オーバーフローする値が伝播され、後で同様のオーバーフロー行が発生する可能性があります。既定で、Code Prover には同様のオーバーフローの最初のものしか表示されません。すべてのオーバーフローを表示するには、オプション [同様のオーバーフローを表示する] (-show-similar-overflows) (Polyspace Code Prover) を使用します。

ヒント

  • 符号なし整数から同じサイズの符号付き整数への変換におけるオーバーフローをチェックするには、[符号なし整数のオーバーフロー モード] を [forbid] または [warn-with-wrap-around] に設定します。符号なし整数のオーバーフローを許容すると、符号付き整数のオーバーフローをチェックしている場合でも、Polyspace は変換におけるオーバーフローにフラグを設定せず、オーバーフローの結果をラップします。

  • Polyspace Code Prover では、オーバーフローした符号なし定数をラップします。オプションを使用してこの動作を変更することはできません。符号なし定数でのオーバーフローを検出する場合は、Polyspace Bug Finder™ のチェッカー [符号なし整数定数のオーバーフロー] を使用します。

  • Code Prover は符号なし変数または sbit に対するビット演算でのオーバーフローを示しません。たとえば、この例では次のようになります。

    volatile unsigned char Y;
Y = ~Y;
    検証では、このようなビット演算は計画的なものであり、演算の結果がオーバーフローした場合の自動ラップアラウンドが意図されていると見なします。

コマンド ライン情報

パラメーター: -unsigned-integer-overflows
値: forbid | allow | warn-with-wrap-around
既定値: allow
例 (Code Prover): polyspace-code-prover -sources file_name -unsigned-integer-overflows allow
例 (Code Prover Server): polyspace-code-prover-server -sources file_name -unsigned-integer-overflows allow

バージョン履歴

R2018b で導入

参考

| (Polyspace Code Prover) | (Polyspace Code Prover)

トピック