ウォーム リブート後にグローバル変数が初期化されることをチェック (-check-globals-init)

グローバル変数が設計された初期化コードで割り当てられた値であることのチェック

説明

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

宣言時、または初期化コードとしてマークされたコードのセクションで、すべての非 const グローバル変数 (およびローカルの静的変数) が明示的に初期化されているかどうかを Polyspace® でチェックすることを指定します。

初期化コードは、検証対象のソース コードによって異なります。

  • アプリケーション全体を検証する場合 — 初期化コードは main() 関数の先頭から始まり、この #pragma 命令まで継続します。

    #pragma polyspace_end_of_init
    この #pragma を複数指定することはできません。コンパイラは認識されないプラグマを無視するため、このプラグマが存在してもプログラムの実行には影響しません。

  • モジュールまたはライブラリを検証する場合 — 初期化コードは、生成される main よりも前に呼び出される一連の関数です。オプション [初期化関数] (-functions-called-before-main) を使用してこれらの関数を指定します。Polyspace は、初期化関数がその指定順序で呼び出されると想定します。

オプションの設定

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

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

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

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

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

ウォーム リブートでは、時間短縮のため、プログラムのシンボル (bss) セグメントで始まるブロック (以前の状態の変数値を保持している可能性がある領域) が読み込まれません。代わりに、プログラムが実行前に既定値を持たないすべての非 const 変数を明示的に初期化することが想定されています。このオプションを使用して、初期化コードを区切り、すべての非 const グローバル変数がウォーム リブートで初期化されることを検証できます。

たとえば、次の簡単な例では、初期化コード セクションでグローバル変数 aVar は初期化されますが、変数 anotherVar は初期化されません。

int aVar;
const int aConst = -1;
int anotherVar;

int main() {
      aVar = aConst;
#pragma polyspace_end_of_init
      return 0;
}

設定

オン

Polyspace は、すべてのグローバル変数が指定された初期化コードで初期化されるかどうかをチェックします。初期化コードは、main 関数の先頭から始まり、プラグマ polyspace_end_of_init まで継続します。

[初期化コードでグローバル変数に値が割り当てられていません] を使用したチェック結果が報告されます。

オフ (既定の設定)

Polyspace は、指定されたコード セクションでのグローバル変数の初期化をチェックしません。

ただし、検証では、変数が使用時に初期化されているかどうかのチェックは続行されます。この結果は、[未初期化変数] チェックを使用して報告されます。

依存関係

ヒント

  • このオプションをオプション [コードの初期化セクションのみの検証] (-init-only-mode) と併用すると、残りのプログラムをチェックする前に初期化コードをチェックできます。

    この方法には、1 回の実行でコード全体をチェックする方法に比べて以下の利点があります。

    • 初期化コードのランタイム エラーによって、残りのコードの解析が無効になることがあります。残りのプログラムをチェックする前に初期化コードをチェックすると、比較的短時間でチェックを実行できます。

    • [初期化コードでグローバル変数に値が割り当てられていません] チェックの結果は、比較的簡単に確認できます。

      以下の例を考えてみます。if および else if ステートメントがスキップされたときに var が初期化されない可能性があるため、var に対するオレンジ チェックが発生します。

      int var;
 
int checkSomething(void);
int checkSomethingElse(void);
 
int main() {
    int local_var;
    if(checkSomething())
    {
        var=0;
    }
    else if(checkSomethingElse()) {
        var=1;
    }
    #pragma polyspace_end_of_init
    var=2;
    local_var = var;
    return 0;
}

      このチェックを確認して、どのような場合に x が初期化されないかを理解するには、[変数アクセス] ペインで x のすべてのインスタンスを参照する必要があります。初期化コードのみをチェックする場合、太字のコードのみがチェックされ、初期化コードのインスタンスのみを参照するだけで済みます。

  • このチェックを使用する際のベスト プラクティスは、初期化コードを正しく指定することです。以下に例を示します。

    • グローバル変数のすべての初期化が対象となるように初期化コードを指定します。つまり、命令 #pragma polyspace_end_of_init を初期化の末尾より後に配置します。あるいは、モジュールの検証時に、初期化を実行するすべての関数を指定します。このようにしないと、Polyspace は、マークされた初期化コードの外部で初期化される変数に対し、未初期化としてフラグを設定します。

    • 命令 #pragma polyspace_end_of_init をブロック内に配置しないようにします。プラグマをブロック内に配置すると、そのブロック内で終了しないパスが、このチェックから除外されます。

      ブロック内で終了するすべてのパスで変数が初期化されても、ブロックをスキップするパスでは変数が初期化されないままになる可能性があります。プラグマをブロック内に配置する場合は、ブロックの外部で変数が初期化されていなくても問題ないことを確認してください。

      たとえば、次の例では、プラグマのある場所で終了するすべてのパスで変数 var が初期化されます。if ブロックがスキップされ、変数が初期化されない可能性があるにもかかわらず、このチェックはグリーンになります。

      int var;

int func();

int main() {
    int err = func();
    if(err) {
        var = 0;
 #pragma polyspace_end_of_init
    }
    int a = var;   
    return 0;
}

      プラグマを if ブロックの末尾の後に配置した場合、この問題はチェッカーによって検出されます。

    • 命令 #pragma polyspace_end_of_init をループ内に配置しないでください。

      プラグマをループ内に配置すると、解釈の難しい結果が報告される可能性があります。たとえば、次の例では、aVar と anotherVar の両方がループのいずれかの反復で初期化されています。しかし、初期化に関してグリーン チェックが示される場合、プラグマによってループの最初の反復のみが考慮されます。変数が後の反復で初期化されている場合、チェックはオレンジになります。

      int aVar;
int anotherVar;

void main() {
    for(int i=0; i<=1; i++) {
        if(i == 0)
            aVar = 0;
        else
            anotherVar = 0;
        #pragma polyspace_end_of_init
    }
}
      初期化コードのみを検証し、最初のループ反復で変数を初期化しない場合、チェックはレッドになります。このような誤ったレッド チェックやオレンジ チェックを避けるため、プラグマをループ内に配置しないでください。

    • 通常の Code Prover 解析では、構造体の初期化を判定するため、使用されているフィールドのみが考慮されます。

      オプション [コードの初期化セクションのみの検証] (-init-only-mode) を使用して初期化コードのみをチェックすると、解析ではコードの一部のみが対象となるため、その部分以外で変数が使用されているかどうかを判定できません。このため、初期化のチェックでは、すべての構造体フィールドが (使用されているかどうかに関係なく) 考慮されます。

コマンド ライン情報

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

バージョン履歴

R2020a で導入

すべて展開する

参考

| | |

トピック