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

-preemptable-interrupts

プリエンプタブル割り込みを表す関数の指定

構文

-preemptable-interrupts function1[,function2[,...]]

説明

-preemptable-interrupts function1[,function2[,...]] では、プリエンプタブル割り込みを表す関数を指定します。

この関数は、他の割り込み (プリエンプタブルまたは非プリエンプタブル) から割り込まれる可能性があることを除き、あらゆる場面で割り込みとして機能します。割り込みはオプション [割り込み] (-interrupts) を使用して指定されます。例については、Polyspace でのデータ レース検出のタスク優先順位の定義を参照してください。

関数をプリエンプタブル割り込みとして指定するには、最初に関数を割り込みとして指定しなければなりません。指定する関数は、以下のプロトタイプをもたなければなりません。

void function_name(void);

ユーザー インターフェイス (Polyspace® デスクトップ製品のみ) では、[構成] ペインの [その他] フィールドにこのオプションを入力します。Otherを参照してください。

例

次のプログラムを考えます。関数 task1 および task2 は、割り込みを表しているとします。

int x;
void task1() {
    x++;
}
void task2() {
    x = 0;
}
void main() {
}

task1 と task2 が周期タスクであることを指定するために、以下を入力します。

polyspace-bug-finder -sources filename -interrupts task1,task2
task1 および task2 の演算は互いに割り込むことができないため、[データ レース] 欠陥は表示されません。割り込みとして指定する関数は、既定で非プリエンプタブルです。

task1 をプリエンプタブルとして指定します。

polyspace-bug-finder -sources multi.c -interrupts task1,task2 -preemptable-interrupts task1
task1 の演算 x++ が task2 の演算によって割り込まれる可能性があるため、[データ レース] が表示されるようになります。

ヒント

  • このオプションは、Polyspace as You Code 解析では役立ちません。

  • Code Prover では、このオプションを解釈する際にいくつかの制限があります。その理由は、Code Prover では、すべての操作が非アトミックかつ割り込み可能である可能性があるものと見なされるためです。この過大近似のため、このオプションが無視されているように見える状況になることがあります。例は、Code Prover でのタスクの優先順位の効果を参照してください。

バージョン履歴

R2016b で導入

参考

| | | | |

トピック