時間的に排他なタスク (-temporal-exclusions-file)

同時に実行できないエントリ ポイント関数の指定

説明

同時に実行できないエントリ ポイント関数を指定します。関数の実行は重複できません。

オプションの設定

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

  • Polyspace® ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [マルチタスキング] ノードを選択してから、このオプションの時間的に排他な関数の名前を入力します。最初に有効にしなければならない他のオプションについては、依存関係を参照してください。

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

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

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

このオプションは、マルチタスキング コードの時間的排他を実装するために使用します。

特定のタスクを時間的に排他に指定することによってすべての共有変数が同時アクセスから保護されるかどうかが、Code Prover 検証によってチェックされます。これらの共有変数の取り得る値を決定する際、検証では、時間的に排他なタスクは互いに割り込まないと見なされます。グローバル変数を参照してください。

Bug Finder 解析では、時間的に排他の情報を使用して、データ レースなどの同時実行の欠陥が調査されます。同時実行の欠陥を参照してください。

設定

既定値なし

をクリックしてフィールドを追加します。各フィールドに、スペース区切りの関数のリストを入力します。Polyspace では、リスト内の関数は同時に実行できないものとみなされます。

関数名を手動で入力するか、一覧から選択します。

  • をクリックしてフィールドを追加し、関数名を入力します。

  • をクリックして、コード内の関数の一覧を表示します。その一覧から関数を選択します。

依存関係

デスクトップ製品のユーザー インターフェイスでこのオプションを有効にするには、次のようにします。

これらの関数の一部は、時間的に排他なタスクとして指定できます。あるいは、オプション [外部マルチタスキング構成] で外部ファイルを使用するマルチタスキング構成を指定する場合、外部ファイルの関数の一部を、時間的に排他として指定できます。

自動的に検出されるスレッド作成ルーチン (pthread_create など) では、時間的に排他なタスクを指定することはサポートされていません。これらのルーチンは、個別のスレッドを作成するために、コード内の異なる位置で呼び出すことができます。ただし、時間的に排他のオプションでは、コード内の異なる位置で同一ルーチンの個別の呼び出しを 2 つ指定する操作はサポートされていません。

ヒント

共有変数の取り得る値を判断する際、Code Prover 検証では時間的に排他なタスクの指定が考慮されます。

ただし、共有変数がポインターまたは配列の場合、本ソフトウェアでは、その変数が保護された共有グローバル変数かどうかを判断するためにのみ、この指定が使用されます。Code Prover でランタイム エラーをチェックしている場合、本ソフトウェアではこの指定が考慮されず、その変数は同時にアクセスされる可能性があると見なされます。

コマンド ライン情報

コマンド ライン オプションでは、次の形式で時間的排他ファイルを作成します。

  • 各行に、時間的に排他なタスクのグループを 1 つずつ入力します。

  • 行内のタスクはスペースで区切ります。

コメントの入力は # から開始します。例は、ファイル polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\temporal_exclusions.txt を参照してください。ここで、polyspaceroot は Polyspace インストール フォルダーです。たとえば、C:\Program Files\Polyspace\R2019a です。

パラメーター: -temporal-exclusions-file
既定値なし
値: 時間的排他ファイルの名前
例 (Bug Finder): polyspace-bug-finder -sources file_name -temporal-exclusions-file "C:\exclusions_file.txt"
例 (Code Prover): polyspace-code-prover -sources file_name -temporal-exclusions-file "C:\exclusions_file.txt"
例 (Bug Finder Server): polyspace-bug-finder-server -sources file_name -temporal-exclusions-file "C:\exclusions_file.txt"
例 (Code Prover Server): polyspace-code-prover-server -sources file_name -temporal-exclusions-file "C:\exclusions_file.txt"

参考

| | | | |

トピック