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

コードの初期化セクションのみの検証 (-init-only-mode)

初期化コードのみのランタイム エラーとその他の問題のチェック

説明

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

初期化コードとしてマークされたコードのセクションのみのランタイム エラーとその他の問題を Polyspace® でチェックすることを指定します。

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

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

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

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

オプションの設定

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

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

  • Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [実行時エラー] ノードを選択してから、このオプションを選択します。このオプションのその他の要件については、依存関係を参照してください。

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

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

多くの場合、初期化コードに問題があると、残りのコードの解析は無効になります。このオプションを使用して初期化コードのみをチェックし、問題を修正してから、このオプションを無効にして残りのプログラムを検証することができます。

以下の例を考えてみます。

  • アプリケーション全体の検証 — このサンプル コードには main() 関数が含まれており、完全なアプリケーションと見なされます。初期化コードの最後は、プラグマ指令 polyspace_end_of_init によって示されます。 

    #include <limits.h>

int aVar;
const int aConst = INT_MAX;
int anotherVar;

int main() {
      aVar = aConst + 1;
#pragma polyspace_end_of_init
      anotherVar = aVar - 1;
      return 0;
}
    この例では、後のコードで aVar の値を使用する前に、行 aVar = aConst+1 のオーバーフローを修正しなければなりません。

  • モジュールまたはライブラリの検証 — このサンプル コードには main() 関数が含まれておらず、モジュールまたはライブラリと見なされます。初期化コードとその順序は、オプション [初期化関数] (-functions-called-before-main) で指定されます。

    #include <limits.h>

int aVar;
const int aConst = INT_MAX;
int anotherVar;

void initialize() {
	aVar = aConst + 1;
}

int foo() {
	anotherVar = aVar - 1;
	return 0;
}
    この例では、後のコードで aVar の値を使用する前に、行 aVar = aConst+1 のオーバーフローを修正しなければなりません。この例では次のコマンドを使用します。
    polyspace-code-prover -sources src.c -init-only-mode -main-generator -functions-called-before-main initialize

設定

オン

Polyspace は、main の先頭からコードをチェックし、プラグマ polyspace_end_of_init まで続行します。

オフ (既定の設定)

Polyspace は、main 関数から始まるアプリケーション全体をチェックします。

依存関係

ヒント

  • 残りのプログラムをチェックする前に初期化コードを十分にチェックするには、このオプションをオプション [ウォーム リブート後にグローバル変数が初期化されることをチェック] (-check-globals-init) と同時に使用します。両方のオプションを使用すると、検証では以下がチェックされます。

    • 初期化コードの明確または潜在的なランタイム エラー。

    • すべての非 const グローバル変数が初期化コードのすべての実行パスで初期化されているかどうか。

  • 初期化コードのみをチェックすると、マルチタスキング オプションは無効になります。これは、タスク (スレッド) が開始する前にグローバル変数の初期化が行われている必要があるためです。このため、タスク本体は検証されません。

    マルチタスキングも参照してください。

  • 初期化コードのみをチェックすると、プラグマを含む実行パスの解析がプラグマのある場所で打ち切られますが、他の実行パスのチェックは続行されます。

    たとえば、次の例では、if ブロック内に pragma が出現します。初期化を含むパスがプラグマのある場所で停止するため、行 int a = var にレッドの [未初期化変数] チェックが表示されます。変数 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;
}
    こうした状況を回避するには、プラグマをブロックの外部に配置してください。この指令の配置に関する推奨事項については、ウォーム リブート後にグローバル変数が初期化されることをチェック (-check-globals-init) を参照してください。

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

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

コマンド ライン情報

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

バージョン履歴

R2020a で導入

すべて展開する

参考

| | |

トピック