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

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

Code Prover で MISRA チェックを実行する場合、一部のチェッカーでは Code Prover 静的解析を内部で使用して MISRA 違反を検出します。Code Prover ではコード内のデータとコントロールフローを正確に追跡するので、Code Prover の MISRA チェッカーは Bug Finder よりも厳密です。次に例を示します。

:このルールでは、"the value of an object with automatic storage duration shall not be read before it has been set" を規定しています。Code Prover では、未初期化ローカル変数 (Polyspace Code Prover)チェックの結果を使用してルール違反を判別します。
MISRA C™: 2004 Rule 13.7:このルールでは、"Boolean operations whose results are invariant shall not be permitted" を規定しています。Code Prover では、到達不能コード (Polyspace Code Prover)チェックの結果を使用して常に true または false である条件を特定します。

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

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

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

データ型の変換のルール

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

次の例では、行 temp = var1 - var2; がに違反しています。このルールでは、式の値は、異なる実質的な型カテゴリのオブジェクトには代入されないことを規定しています。ここで、2 つの int 変数の差が char 変数に代入されます。Code Prover オーバーフロー (Polyspace 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; の = をクリックします。想定される MISRA C:2012 Rule 10.3 の違反が表示され、[オーバーフロー] のグリーンチェックも表示されます。

The Result Details pane shows both an overflow and a violation of MISRA C:2012 Rule 10.3.

このグリーンチェックは、int から char への変換でオーバーフローが発生しないことを示します。

The Result Details pane shows that the conversion operation from int32 to int8 type does not overflow.

オーバーフローのグリーンチェックを根拠として使用して、ルール違反を正当化できます。

ポインター演算のルール

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

次の例では、演算 ptr++ が MISRA C:2004 Rule 17.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++;
    }
    return 0;
}

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

このコードに Code Prover を実行します。[ソース] ペインで、ptr++ の ++ をクリックします。想定される MISRA C:2004 Rule 17.4 の違反が表示されます。

The Result Details pane shows a violation of MISRA C:2004 Rule 17.4.

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

The Result Details pane shows that the pointer 'ptr' is dereferenced within its bounds. The pointer is not null and pointers to 1 byte at offset [0 ..17] in a buffer of 18 bytes, so is within bounds.

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

参考

トピック

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