割り込み (`-interrupts`)

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

説明

非プリエンプタブル割り込みを表す関数を指定します。解析では、関数本体内の操作に対して以下が仮定されます。

任意の回数を実行できます。
非周期のタスク、周期タスク、および他の割り込みから割り込まれる可能性はありません。非周期のタスクはオプション [タスク] (-entry-points) を使用して指定され、周期タスクはオプション [周期タスク] (-cyclic-tasks) を使用して指定されます。
割り込みをプリエンプタブルにすることもできます。
- 他の割り込みから割り込まれる可能性のある割り込みをモデル化するには、その割り込みをプリエンプタブルに指定します。-preemptable-interrupts を参照してください。例については、Polyspace でのデータレース検出のタスク優先順位の定義を参照してください。
- 割り込みのセクションのみをプリエンプタブルにするには、そのセクションの前にすべての割り込みを有効にするルーチンを呼び出し、セクションが完了してからすべての割り込みを無効にする、別のルーチンを呼び出します。たとえば、ルーチン isr() を割り込みとして指定すると、既定で非プリエンプタブルになります。ただし、isr() 内では、すべての割り込みを有効にするルーチンを呼び出すと、その呼び出しに続くセクションが、すべての割り込みを無効にする別のルーチンを呼び出すまで、プリエンプタブルになります。
```
void isr() {
   x++; //Nonpreemptable
   enable_all_interrupts(); //Routine enabling interrupts
   y++; //Preemptable
   disable_all_interrupts(); //Routine disabling interrupts
   z++; //Nonpreemptable
}
```
  すべての割り込みを有効または無効にする方法については、すべての割り込みを無効にする (-routine-disable-interrupts -routine-enable-interrupts) を参照してください。

オプションの設定

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

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

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

このオプションを使用して、マルチタスキングコードの割り込みを指定します。指定する関数は、以下のプロトタイプをもたなければなりません。

void function_name(void);

Bug Finder 解析では、この指定を使用して、同時実行の欠陥が調査されます。データレース欠陥の場合、解析では割り込みと他のタスクの間に以下の関係が確立されます。

2 つの割り込み間のデータレース:
異なる割り込み内の 2 つの操作は (いずれかの割り込みがプリエンプタブルでない限り) 互いに干渉する可能性はありません。保護されていない同じ共有変数を使用する操作でも、データレースが発生する可能性はありません。
割り込みと別のタスクとの間のデータレース:
- 割り込み内の操作が他のタスクのアトミック操作に干渉する可能性はありません。保護されていない同じ共有変数を使用する操作でも、データレースが発生する可能性はありません。
- 割り込み内の操作は、他のタスクも非プリエンプタブルでない限り、他のタスク内の非アトミック操作に干渉する可能性があります。したがって、保護されていない同じ共有変数を使用する操作では、データレースが発生する可能性があります。

詳細は、次を参照してください。

Code Prover 検証では、この指定を使用して以下が判断されます。

グローバル変数が共有されているかどうか。
グローバル変数 (Polyspace Code Prover)を参照してください。
ランタイムエラーが発生する可能性があるかどうか。
たとえば、演算 var=INT_MAX; が割り込みで行われ、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 でのタスクの優先順位の効果 (Polyspace Code Prover)を参照してください。

コマンドライン情報

パラメーター: -interrupts

既定値なし

値: function1[,function2[,...]]

例 (Bug Finder): polyspace-bug-finder -sources file_name -interrupts func_1,func_2

例 (Code Prover): polyspace-code-prover -sources file_name -interrupts func_1,func_2

例 (Bug Finder Server): polyspace-bug-finder-server -sources file_name -interrupts func_1,func_2

例 (Code Prover Server): polyspace-code-prover-server -sources file_name -interrupts func_1,func_2

バージョン履歴

R2016b で導入

参考

割り込み (-interrupts)

説明