メインコンテンツ

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

Variable Access

ソース コード内のグローバル変数アクセスを示すテーブルの作成 (Code Prover のみ)

説明

このコンポーネントは、ソース コード内のグローバル変数アクセスを示すテーブルを作成します。グローバル変数ごとに、このテーブルは以下の情報を表示します。

  • 変数名。

    各レベルは | で表されます。

  • 変数のデータ型。

  • 変数の読み取りと書き込み操作の数。

  • 読み取りと書き込み操作の詳細。読み取りと書き込みの操作ごとに、以下の情報が表内に表示されます。

    • file_name.function_name の形式で操作を含むファイルおよび関数。

      エントリは読み取りまたは書き込みの操作ごとに || で表されます。書き込み操作は < で、読み込み操作は > で表されます。

    • 操作の行番号と列番号。

このテーブルは Polyspace® ユーザー インターフェイスの [変数アクセス] ペインで使用可能な情報を表示します。

変数アクセスを表示するテーブルには、ファイル名のみが記載されます。このテーブルの下にある 2 つ目のテーブルには、ファイルへの絶対パスが ([ファイル名][完全なファイル名] の 2 つの列に) 表示されます。標準ライブラリ関数で変数アクセスが発生した場合、この 2 つの列には次の情報が記載されます。

  • ファイル名: __polyspace__stdstubs.c (標準ライブラリ関数の Polyspace 実装を含むファイル)

  • 完全なファイル名:標準ライブラリ