初期化する変数 (-main-generator-writes-variables)

生成された main により初期化するグローバル変数の指定

説明

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

このオプションは、MATLAB® コードまたは Simulink® モデルから生成されたコードでは使用できません。

生成された main で初期化するグローバル変数を指定します。Polyspace® では、それらの変数が型に応じた任意の値をもつと見なします。

オプションの設定

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

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

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

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

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

モジュールまたはライブラリを検証している場合、main 関数が存在しないと、Code Prover によって生成されます。main 関数が存在する場合、解析では既存の main が使用されます。

関数 main のないモジュールの Code Prover 解析では、グローバル変数の初期化について、既定の仮定が行われます。解析では、明示的に初期化されないグローバル変数のそれぞれは、呼び出されない関数に入るたびに、そのデータ型で許容される全範囲の値を取るものと仮定されます。たとえば、関数 main がない以下の例では、変数 glob は (foo での変更にもかかわらず) foo と bar の両方で考えられる "すべて" の int 値を取るものと仮定されます。どちらの関数が先に呼び出されるのかを含め、foo と bar の呼び出しのコンテキストは不明であるため、この仮定は保守的なものです。

int glob;

int foo() {
   int locFoo = glob;
   glob++;
   return locFoo;
}

int bar() {
   int locBar = glob;
   return locBar;
}
この仮定を実装するために、main の生成では、このようなグローバル変数を全範囲の値に初期化してから、変数が初期化されなければ呼び出されない各関数を呼び出します。この既定の仮定を変更して、グローバル変数の別の初期化手法を実装するには、このオプションを使用します。

設定

既定値: public

uninit

生成された main は、宣言時に初期化されなかったグローバル変数のみを初期化します。

none

生成された main はグローバル変数を初期化しません。

グローバル変数は、C/C+ 規格に従って初期化されます。たとえば、変数 int または char は 0 に初期化され、変数 float は 0.0 に初期化されるといった具合です。

public

生成された main は、キーワード static および const で宣言された変数を除くグローバル変数をすべて初期化します。

all

生成された main は、キーワード const で宣言された変数を除くグローバル変数をすべて初期化します。

custom

生成された main は、指定されたグローバル変数のみを初期化します。Add row to table icon. をクリックしてフィールドを追加します。グローバル変数名を入力します。

依存関係

オプション [モジュールまたはライブラリの検証] (-main-generator) (Polyspace Code Prover) が選択されている場合にのみ、このオプションを使用できます。

次の場合、このオプションは無視されます。

ヒント

このオプションは、プロジェクトで定義されているグローバル変数にのみ影響します。グローバル変数が extern として宣言されている場合、解析では、このオプションの値に関係なく、その変数がそのデータ型によって許容される任意の値を取る可能性があることが考慮されます。

コマンド ライン情報

パラメーター: -main-generator-writes-variables
値: uninit | none | public | all | custom=variable1[,variable2[,...]]
既定値: public
例 (Code Prover): polyspace-code-prover -sources file_name -main-generator -main-generator-writes-variables all
例 (Code Prover Server): polyspace-code-prover-server -sources file_name -main-generator -main-generator-writes-variables all

バージョン履歴

すべて展開する

参考

トピック