グローバル変数の初期化に関する Code Prover の仮定

グローバル変数は、プログラム全体で (ローカル変数より優先順位が低くない限り) 可視となる変数です。Code Prover 解析では、グローバル変数の初期化について特定の仮定を行います。

main 関数が存在する場合のグローバル変数の初期化

コードに main 関数が含まれている場合、Code Prover 検証では、グローバル変数は ANSI® C 規格に従って初期化されると見なされます。既定値は、以下のとおりです。

  • int では 0

  • char では 0

  • float では 0.0

などが挙げられます。

場合によっては、グローバル変数がコード内で明示的に初期化されているかどうかをチェックする必要があります。次に例を示します。

main 関数が存在しない場合のグローバル変数の初期化

コードに main 関数がない場合、Code Prover では、グローバル変数がデータ型によってのみ制約された全範囲の値を取ると仮定され、"呼び出されていない" 各関数の検証が開始されます。データ型からの変数範囲に関する Code Prover の仮定も参照してください。

たとえば、以下の例を考えてみます。

int glob;
void func1_callee();

void func1() {
    int loc =  glob;
    if(!glob)
       func1_callee();
}

void func1_callee() {
    int loc = glob;
}

void func2() {
    int loc = glob;
}
func1 と func2 のどちらでも、グローバル変数 glob と (結果的に) ローカル変数 loc は int の全範囲の値を取ります。

しかし、グローバル変数の全範囲の値で始まるのは、呼び出されていない関数だけです。関数 func1_callee は、func1 で glob がゼロに制約された後で呼び出されています。func1_callee では、グローバル変数 glob と (結果的に) ローカル変数 loc が制約された値 0 を取ります。

Code Prover でグローバル変数の初期化に関する仮定がどのように実装されているか

ソフトウェアではダミー関数 _init_globals() を使用して、グローバル変数を初期化します。関数 _init_globals() は、main 関数 (main 関数がない場合は、生成された main 関数) で暗黙的に呼び出される最初の関数です。

アプリケーション gv_example.c で以下のコードを考えます。

extern int func(int);

int garray[3] = {1, 2, 3};  
int gvar = 12;

int main(void) {
    int i, lvar = 0;
    for (i = 0; i < 3; i++) 
       lvar += func(garray[i] + gvar);
    return lvar;
}

検証後は次のようになります。

  • [結果のリスト] ペインで のリストから [ファイル] を選択すると、gv_example.c ノードに _init_globals が表示されます。

    The Results List pane shows the function '_init_globals' followed by a list of global variables initialized in this function.

  • [変数アクセス] ペインで、gv_example._init_globals はグローバル変数の初期化を表しています。[値] 列には、初期化直後のグローバル変数の値が表示されます。

    The Variable Access pane shows the initialization of global variables as write operations in the '_init_globals' function.

複素数データ型の初期化が何を意味するか

次の表は、各データ型で初期化を判定するためにチェックされる内容を示しています。このチェックは、読み取り操作時のチェック [未初期化変数] と、初期化セクションの終了時のチェック [初期化コードでグローバル変数に値が割り当てられていません] で行われます。

データ型初期化のグリーン チェックが何を意味するか
基本型 (int、double など)変数が少なくとも 1 回書き込まれています。
配列データ型すべての配列要素が少なくとも 1 回書き込まれています。
構造化データ型

使用されているすべての構造体フィールドが少なくとも 1 回書き込まれています。

オプション [コードの初期化セクションのみの検証] (-init-only-mode) のみを使用して初期化コードをチェックする場合、解析では、使用されているかどうかに関係なく、すべての構造体フィールドの初期化がチェックされます。

どのフィールドも使用されない特殊なケースでは、すべてのフィールドが初期化されていない場合に初期化のチェックがグリーンではなくオレンジになります。

ポインターポインターが少なくとも 1 回書き込まれています。ただし、Code Prover では、参照されているバッファーの初期化は (ポインターをデリファレンスするまで) チェックされません。
列挙型enum 変数が少なくとも 1 回書き込まれています。ただし、Code Prover では、変数の値が enum 値の 1 つであるかどうかはチェックされません。

参考

| | |