このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。
周期タスク (-cyclic-tasks
)
周期タスクを表す関数の指定
説明
周期タスクを表す関数を指定します。解析では、関数本体内の操作に対して以下が仮定されます。
任意の回数を実行できます。
非周期のタスク、他の周期タスク、および割り込みから割り込まれる可能性があります。非周期のタスクはオプション
[タスク] (-entry-points)
を使用して指定され、割り込みはオプション[割り込み] (-interrupts)
を使用して指定されます。他の周期タスクから割り込まれる可能性のない周期タスクをモデル化するには、そのタスクを非プリエンプタブルに指定します。
-non-preemptable-tasks
を参照してください。例については、Polyspace でのデータ レース検出のタスク優先順位の定義を参照してください。
オプションの設定
以下のいずれかの方法を使用してオプションを設定します。
Polyspace® ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [マルチタスキング] ノードを選択してから、このオプションの関数名を入力します。最初に有効にしなければならない他のオプションについては、依存関係を参照してください。
Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [マルチタスキング] ノードを選択してから、このオプションの関数名を入力します。最初に有効にしなければならない他のオプションについては、依存関係を参照してください。
コマンド ラインとオプション ファイル: オプション
-cyclic-tasks
を使用します。コマンド ライン情報を参照してください。
このオプションを使用する理由
このオプションを使用して、マルチタスキング コードの周期タスクを指定します。指定する関数は、以下のプロトタイプをもたなければなりません。
void function_name(void);
Bug Finder 解析では、この指定を使用して、同時実行の欠陥が調査されます。データ レース
欠陥の場合、本ソフトウェアではプリエンプタブルなタスクと他のタスクの間に以下の関係が確立されます。
プリエンプタブルな 2 つのタスク間のデータ レース:
保護される場合を除き、プリエンプタブルな異なるタスクの 2 つの操作は、相互に干渉する可能性があります。保護されていない同じ共有変数を使用する操作では、データ レースが発生する可能性があります。
両方の操作がアトミックの場合、この欠陥を確認するにはチェッカー [データ レースに Atomic の演算が含まれています] を有効にする必要があります。
プリエンプタブルなタスクと、非プリエンプタブル タスクまたは割り込みとの間のデータ レース:
プリエンプタブルなタスク内のアトミック操作は、非プリエンプタブル タスクまたは割り込みの操作に干渉する可能性はありません。保護されていない同じ共有変数を使用する操作でも、データ レースが発生する可能性はありません。
プリエンプタブルなタスク内の非アトミック操作も、非プリエンプタブル タスクまたは割り込みの操作に干渉する可能性はありません。ただし、後者の操作が前者の操作に干渉する可能性はあります。したがって、保護されていない同じ共有変数を使用する操作では、データ レースが発生する可能性があります。
詳細は、次を参照してください。
Code Prover 検証では、この指定を使用して以下が判断されます。
グローバル変数が共有されているかどうか。
グローバル変数を参照してください。
ランタイム エラーが発生する可能性があるかどうか。
たとえば、演算
var++
が周期タスクの本体内で行われ、var
に制限を設けていない場合、この演算はオーバーフローする可能性があります。解析により、オーバーフローが発生する可能性が検出されます。
設定
既定値なし
関数名を入力するか、一覧から選択します。
をクリックしてフィールドを追加し、関数名を入力します。
をクリックして、コード内の関数の一覧を表示します。その一覧から関数を選択します。
依存関係
デスクトップ製品のユーザー インターフェイスでこのオプションを有効にするには、最初にオプション [マルチタスクを手動で構成]
を選択します。
ヒント
Code Prover では、周期タスクを表す関数は次の形式に準拠しなければなりません。
void functionName (void)
関数
func
が引数を取るか、値を返す場合は、この関数を周期タスクとして直接使用することはできません。func
を周期タスクとして使用するには、ラッパーvoid
-void
関数からfunc
を呼び出して、そのラッパーを周期タスクとして指定します。Polyspace マルチタスキング解析の手動設定を参照してください。関数を周期タスクとして指定する場合、その定義を指定しなければなりません。そうしないと、Code Prover 検証が停止してエラー メッセージが表示されます。
task func_name must be a userdef function without parameters
Bug Finder 解析は続行されますが、その関数は周期タスクとは見なされません。
Code Prover でファイルごとの検証を実行する場合、マルチタスキング オプションは無視されます。
ファイルを個別に検証 (-unit-by-unit)
を参照してください。Polyspace マルチタスキング解析は、タスクがそれ自身に割り込む可能性がないことを前提としています。
Code Prover では、このオプションを解釈する際にいくつかの制限があります。その理由は、Code Prover では、すべての操作が非アトミックかつ割り込み可能である可能性があるものと見なされるためです。この過大近似のため、このオプションが無視されているように見える状況になることがあります。例は、Code Prover でのタスクの優先順位の効果を参照してください。
コマンド ライン情報
パラメーター: -cyclic-tasks |
既定値なし |
値:
|
例 (Bug Finder): polyspace-bug-finder -sources |
例 (Code Prover): polyspace-code-prover -sources |
例 (Bug Finder Server): polyspace-bug-finder-server -sources |
例 (Code Prover Server): polyspace-code-prover-server -sources |
バージョン履歴
R2016b で導入