このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

符号付き整数のオーバーフロー モード (-signed-integer-overflows)

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

説明

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

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

オプションの設定

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

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

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

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

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

このオプションを使用して、符号付き整数のオーバーフローをチェックするかどうかを指定し、オーバーフロー後に解析の前提とされる内容を指定します。

設定

既定値: forbid

forbid

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

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

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

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

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

この動作は、ANSI C (ISO C++) 規格に適合します。

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

#include<stdio.h>

int getVal();

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

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

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

allow

Polyspace は符号付き整数のオーバーフローにフラグを設定しません。演算の結果としてオーバーフローが発生した場合、Polyspace は残りのコードを解析しますが、オーバーフローの結果をラップします。

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

#include<stdio.h>

int getVal();

void func1()
{
    int i = 1;
    i = i << 30;
    // i = 230
    i = i * 2;
    // i = -231
    printf("%d", i);
}
void func2()
{

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

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

warn-with-wrap-around

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

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

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

#include<stdio.h>

int getVal();

void func1()
{
    int i = 1;
    i = i << 30;
    // i = 230
    // Result of * operation overflows
    i = i * 2;
    // i = -231
    printf("%d", i);
}
void func2()
{

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

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

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

ヒント

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

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

コマンド ライン情報

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

バージョン履歴

R2018b で導入

参考

| |

トピック