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

Code Prover チェックを使用したコーディング ルール違反の正当化

コーディング ルールは、安心で安全なコードを確認するためのベスト プラクティスです。Polyspace^® コーディング ルール チェッカーを使用して、MISRA™ C:2023 などのコーディング ルール規格に違反している、コード内のインスタンスを検出します。Code Prover を実行する場合、ランタイム エラーを検出したか否かのチェックの結果も表示されます。場合によっては、2 種類の結果を使用することで効率的なレビューができます。たとえば、コーディング ルール違反を修正 (正当化) しない根拠としてグリーンの Code Prover チェックを使用できます。次に例を示します。

• MISRA C:2012 Rule 9.1 および MISRA C:2023 Rule 9.1:このルールでは、"the value of an object with automatic storage duration shall not be read before it has been set" を規定しています。未初期化ローカル変数チェックの結果を使用して、ルール違反を正当化します。

• MISRA C™: 2004 Rule 13.7:このルールでは、"Boolean operations whose results are invariant shall not be permitted" を規定しています。到達不能コードチェックの結果を使用して、常に true または false となる条件を特定します。

対応するグリーン チェックによって違反が影響を及ぼさないことが示されている場合でも、MISRA チェッカーによってルール違反が表示されます。次のいずれかを実行する選択肢があります。

• 規格に厳密に準拠し、ルール違反を修正する。

• グリーン チェックを根拠として使用してルール違反を手動で正当化する。

  [アクションの予定なし] などのステータスを結果に設定し、結果のコメントにグリーン チェックを根拠として入力します。後で、このステータスを使用して、正当化済み結果をフィルターにより除外できます。

以下の節では、Code Prover のグリーン チェックを使用して MISRA 違反を正当化できる状況の例を説明します。

データ型の変換のルール

変換によってオーバーフローが発生しない場合は、暗黙的なデータ型の変換ができることがあります。

次の例では、行 temp = var1 - var2; が MISRA C:2023 Rule 10.3 に違反しています。このルールでは、式の値は、異なる実質的な型カテゴリのオブジェクトには代入されないことを規定しています。ここで、2 つの int 変数の差が char 変数に代入されます。Code Prover オーバーフローチェックの結果を使用して、この特定のルール違反を正当化できます。

int func (int var1, int var2) {
    char temp;
    temp = var1 - var2;
    if (temp > 0)
        return -1;
    else
        return 1;
}

double read_meter1(void);
double read_meter2(void);

int main(char arg, char* argv[]) {
    int meter1 = (read_meter1()) * 10;
    int meter2 = (read_meter2()) * 999;
    int tol = 10;
    if((meter1 - meter2)> -tol && (meter1 - meter2) < tol)
        func(meter1, meter2);
    return 0;
}

このルールの背景にある根拠について考えます。異なる型の間で暗黙的な変換を使用すると、値、符号、精度の損失の可能性を含め、意図しない結果を引き起こす場合があります。int から char への変換では、符号や精度の損失は発生しません。唯一の問題は、2 つの int 変数の差がオーバーフローする場合に値が損失する可能性があることです。

このコードに Code Prover を実行します。[ソース] ペインで、temp = var1 - var2; の = をクリックします。グリーンの [オーバーフロー] チェックが表示されます。このグリーン チェックは、int から char への変換でオーバーフローが発生しないことを示します。オーバーフローのグリーン チェックを根拠として使用して、ルール違反を正当化できます。

ポインター演算のルール

ポインターが許容されるバッファー内にある場合は、非配列ポインターに対するポインター演算ができます。

次の例では、演算 ptr += 1 が MISRA C:2023 Rule 18.4 に違反しています。このルールに違反しているのは、ポインター型の式での演算子 += の使用は推奨されていないためです。

#define NUM_RECORDS 3
#define NUM_CHARACTERS 6

void readchar(char);   

int main(int argc, char* argv[]) {
    char dbase[NUM_RECORDS][NUM_CHARACTERS] = { "r5cvx", "a2x5c", "g4x3c"};
    char *ptr = &dbase[0][0];
    for (int index = 0; index < NUM_RECORDS * NUM_CHARACTERS; index++) {
        readchar(*ptr);
        ptr += 1; //Violation of 18.4
    }
    return 0;
}

このルールの背景にある根拠について考えます。インクリメントの後、ポインターが許容されるバッファー (配列など) の範囲外になるか、任意の場所を指す可能性があります。ポインターが許容されるバッファー内を指している限り、ポインター演算は問題ありません。Code Prover 不適切にデリファレンスされたポインターチェックの結果を使用して、この特定のルール違反を正当化できます。

このコードに Code Prover を実行します。[ソース] ペインで、ptr++ の ++ をクリックします。演算 readchar(*ptr) の * をクリックします。[不適切にデリファレンスされたポインター] のグリーン チェックが表示されます。このグリーン チェックは、デリファレンスされた場合にポインターが許容範囲内を指すことを示します。

このグリーン チェックを使用して、ルール違反を正当化できます。

参考

トピック

• Polyspace ユーザー インターフェイスでのバグ修正または正当化による結果への対処