未初期化のチェックを無効にする (-disable-initialization-checks)

未初期化変数および未初期化ポインターのチェックの無効化

説明

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

Polyspace® Code Prover™ でコード内の未初期化がチェックされないよう指定します。

オプションの設定

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

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

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

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

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

未初期化変数のインスタンスを検出しない場合は、このオプションを使用します。

設定

オン

Polyspace Code Prover で以下のチェックは実行されません。

Polyspace では、宣言時に以下が想定されます。

  • 変数は、そのデータ型で許容される全範囲の値をもつ。

  • ポインターは NULL 値を取るか、不明なオフセットでメモリ ブロックを指す。

オフ (既定の設定)

Polyspace Code Prover でコード内の未初期化がチェックされます。変数が初期化されていない場合などには、レッド チェックが表示されます。変数が一部の実行パスでのみ初期化されている場合は、オレンジ チェックが表示されます。

ヒント

  • このオプションを選択すると、MISRA C™:2004 Rule 9.1 および MISRA C:2012 Rule 9.1 でのほとんどの違反はレポートされません。

  • このオプションを選択すると、コード内のオレンジ チェックの数やタイプが変更される場合があります。

    たとえば、次の表では、オプションを有効にするとオレンジ チェックが追加されることが説明されています。

    未初期化のチェックが有効未初期化のチェックが無効
    void func(int flag) {
    int var1,var2;
    if( flag==0) {
        var1=var2;
    }
    else {
        var1=0;
    }
    var2=var1 + 1;
}

    この例では、ソフトウェアにより以下が生成されます。

    • if 分岐での var2 に関する [未初期化ローカル変数] のレッド チェック検証は if ステートメントの else 分岐のみが存在するかのように継続されます。

    • 最後のステートメントでの var1 に関する [未初期化ローカル変数] のグリーン チェック。var1 には値 0 が代入されています。

    • + 演算に関する [オーバーフロー] のグリーン チェック。

    void func(int flag) {
    int var1,var2;
    if( flag==0) {
        var1=var2;
    }
    else {
        var1=0;
    }
    var2=var1 + 1;
}

    この例では、ソフトウェアにより以下が行われます。

    • [未初期化ローカル変数] のチェックは生成されません。初期化に際して、var2 は全範囲の int 値をもつと想定されます。if ステートメントに従って両方の if 分岐が考慮されるため、var1 も全範囲の int 値をもつことが想定されます。

    • + 演算に関する [オーバーフロー] のオレンジ チェックが生成されます。たとえば、var1 が int の最大値である場合、そこに 1 を加算するとオーバーフローの原因となる可能性があります。

コマンド ライン情報

パラメーター: -disable-initialization-checks
既定値: オフ
例 (Code Prover): polyspace-code-prover -sources file_name -disable-initialization-checks
例 (Code Prover Server): polyspace-code-prover-server -sources file_name -disable-initialization-checks

参考

トピック