ISO/IEC TS 17961 [diverr]

Integer division errors

このページをすべて展開する

説明

ルール定義

整数除算エラー。1

Polyspace 実装

このチェッカーは、整数のゼロ除算をチェックします。

チェッカーの拡張

入力値が不明であり、入力のサブセットのみが問題の原因となっている場合、Bug Finder が "整数のゼロ除算" を検出しない場合があります。特定のシステム入力値を原因とする違反の有無をチェックするには、より厳密な Bug Finder 解析を実行してください。特定のシステム入力値から欠陥を見つけるための Bug Finder チェッカーの拡張を参照してください。

例

すべて展開する

問題

整数のゼロ除算は、除算演算またはモジュロ演算の分母 (除数) がゼロ値の整数になる可能性がある場合に発生します。

リスク

ゼロ除算はプログラムをクラッシュさせる可能性があります。

修正方法

修正方法は欠陥の根本原因によって異なります。多くの場合、結果の詳細には欠陥につながる一連のイベントが表示されます。このイベント リストを使用して、分母変数がどのようにゼロ値を取得したのかを確認します。そのシーケンス内のどのイベントについても修正を実装できます。結果の詳細にイベント履歴が表示されない場合は、ソース コード内で右クリック オプションを使用して逆のトレースを行い、これまでの関連するイベントを確認できます。Polyspace デスクトップ ユーザー インターフェイスでの Bug Finder の結果の解釈も参照してください。

除算の前に分母がゼロ値かどうかをチェックしてエラーを処理することをお勧めします。次のように除算を直接実行するのは避けます。

res = num/den;
除算を実行する前に分母のゼロ値を処理するライブラリ関数を使用します。
res = div(num, den);

以下の修正例を参照してください。

問題を修正しない場合は、改めてレビューされないように結果またはコードにコメントを追加します。詳細は、以下を参照してください。

例 - 整数のゼロによる除算
int fraction(int num)
{
    int denom = 0;
    int result = 0;

    result = num/denom;

    return result;
}

denom がゼロであるため、num/denom でゼロ除算エラーが発生します。

修正 — 除算の前にチェック
int fraction(int num)
{
    int denom = 0;
    int result = 0;

    if (denom != 0)
        result = num/denom;

    return result;
}

除算の前に、分母がゼロかどうかを確認するためのテストを追加して、除算が実行される前にチェックします。denom が常にゼロである場合は、この修正により Polyspace® の結果にデッド コードの欠陥が報告される可能性があります。

修正 — 分母を変更

1 つの修正方法として、denom がゼロでなくなるように分母の値を変更することができます。

int fraction(int num)
{
    int denom = 2;
    int result = 0;

    result = num/denom;

    return result;
}
例 - ゼロによるモジュロ演算
int mod_arr(int input)
{
    int arr[5];
    for(int i = 0; i < 5; i++)
    {
        arr[i] = input % i;
    }

    return arr[0]+arr[1]+arr[2]+arr[3]+arr[4];
}

この例では、Polyspace がモジュロ演算にゼロ除算のフラグを立てます。モジュロは本質として除算演算であるため、除数 (右辺引数) をゼロにすることはできません。このモジュロ演算では、除数として for ループのインデックスを使用しています。しかし、for ループはゼロから開始されるので、反復子にはできません。

修正 — 演算の前に除数をチェック

1 つの修正方法として、モジュロ演算の前に除数をチェックします。この例では、モジュロ演算の前に指数 i がゼロかどうかを確認します。

int mod_arr(int input)
{
    int arr[5];
    for(int i = 0; i < 5; i++)
    {
        if(i != 0)
        {
             arr[i] = input % i;
        }
        else
        {
             arr[i] = input;
        }
    }

    return arr[0]+arr[1]+arr[2]+arr[3]+arr[4];
}
修正 — 除数を変更

別の修正方法として、除数を非ゼロの整数に変更します。この例では、% 演算の前に指数に 1 を加算して、ゼロ除算を回避しています。

int mod_arr(int input)
{
    int arr[5];
    for(int i = 0; i < 5; i++)
    {
         arr[i] = input % (i+1);
    }

    return arr[0]+arr[1]+arr[2]+arr[3]+arr[4];
}

チェック情報

決定可能性:決定不可能

バージョン履歴

R2019a で導入

参考

トピック

1 Extracts from the standard "ISO/IEC TS 17961 Technical Specification - 2013-11-15" are reproduced with the agreement of AFNOR. Only the original and complete text of the standard, as published by AFNOR Editions - accessible via the website www.boutique.afnor.org - has normative value.