OIL ファイルの選択 (-osek-multitasking)

OIL ファイル定義からのマルチタスキング構成の設定

説明

OSEK プロジェクトのマルチタスキング構成を設定するために Polyspace^® で解析する OIL ファイルを指定します。

オプションの設定

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

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

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

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

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

プロジェクトに OIL ファイルが含まれる場合、Polyspace ではそれらのファイルを解析して、タスク、割り込み、周期タスク、およびクリティカル セクションを設定できます。それらを手動で設定する必要はありません。

設定

オフ (既定の設定)

Polyspace では OSEK プロジェクトのマルチタスキング構成を設定しません。

オン

Polyspace では OIL を検索、解析して、マルチタスキング構成を設定します。

auto

プロジェクトのソース フォルダーとインクルード フォルダー内で OIL ファイルを検索しますが、サブフォルダー内は検索しません。

custom

指定されたパスとパス サブフォルダーで OIL ファイルを検索します。OIL ファイルのパスまたは OIL ファイルを含むフォルダーのパスを指定できます。

このオプションを選択した場合、ソース コードでは、Polyspace によって以下の OSEK マルチタスキング キーワードがサポートされます。

• TASK

• DeclareTask

• ActivateTask

• DeclareResource

• GetResource

• ReleaseResource

• ISR

• DeclareEvent

• DeclareAlarm

Polyspace では、TASK、ISR、RESOURCE、および ALARM 定義に指定する OIL ファイルを解析します。解析ではこれらの定義とサポートされているマルチタスキング キーワードを使用して、タスク、割り込み、周期タスク、およびクリティカル セクションを構成します。

Polyspace で OIL ファイルから TASK、ISR、および RESOURCE 定義をモデル化する方法を確認するには、[ダッシュボード] ペインで [Concurrency window] を開きます。

Polyspace はタスクがエントリ ポイントであるか周期タスクであるかどうかを判断するために、以下の決定木を使用します。

 例: OSEK マルチタスキング プロジェクトの解析

この例では、OSEK プロジェクトのマルチタスキング構成を設定し、このプロジェクトに対して解析を実行する方法を示します。この例の手順を試すには、フォルダー polyspaceroot/polyspace/examples/doc_cxx/External_multitasking/OSEK または polyspaceroot/polyspace/examples/doc_cxx/External_multitasking/OSEK に含まれるデモ ファイルを使用します。polyspaceroot は Polyspace インストール フォルダーです。解析結果がこのコード例に適用されます。

#include <assert.h>
#include "include/example_osek_multi.h"

int var1; 
int var2; 
int var3; 

DeclareAlarm(Cyclic_task_activate);
DeclareResource(res1);
DeclareTask(init);
TASK(afterinit1);

TASK(init) // task
{
 
  
  var2++;
  ActivateTask(afterinit1);  
  var3++;
  GetResource(res1); // critical section begins
  var1++;
  ReleaseResource(res1); // critical section ends
}

TASK(afterinit1) // task
{
  var3++;
  var2++;
  GetResource(res1); // critical section begins
  var1++;
  ReleaseResource(res1); // critical section ends

}
int var4; 
void func()
{
  var4++; 
}

TASK(Cyclic_task) // cyclic task
{
  func();
}

void main()
{}

マルチタスキング構成を設定してコードを解析するには以下を行います。

1. polyspaceroot\polyspace\examples\doc_cxx\External_multitasking\OSEK の内容をマシンの C:\Polyspace_worskpace\OSEK などにコピーします。

2. 次のコマンドを使用して OSEK プロジェクトの解析を実行します。

   • Bug Finder:

     polyspace-bug-finder -sources ^
     C:\Polyspace_workspace\OSEK\example_osek_multitasking.c ^ 
     -osek-multitasking auto

   • Code Prover:

     polyspace-code-prover -sources ^
     C:\Polyspace_workspace\OSEK\example_osek_multitasking.c ^
     -osek-multitasking auto

   • Bug Finder Server:

     polyspace-bug-finder-server -sources ^
     C:\Polyspace_workspace\OSEK\example_osek_multitasking.c ^ 
     -osek-multitasking auto

   • Code Prover Server:

     polyspace-code-prover-server -sources ^
     C:\Polyspace_workspace\OSEK\example_osek_multitasking.c ^
     -osek-multitasking auto

タスク init および afterinit1 から複数の読み取りおよび書き込み操作が行われるため、Bug Finder では変数 var3 のデータ レースが検出されます。データ レースを参照してください。

#include <assert.h>
#include "include/example_osek_multi.h"

int var1; 
int var2; 
int var3;

init によって var2 がインクリメントされた後、afterinit1 はアクティブ状態になるため (ActivateTask())、var2 に欠陥はありません。同様に、var1 も、GetResource() 呼び出しと ReleaseResource() 呼び出しによって保護されるため、欠陥はありません。

Code Prover は var3 がタスク init および afterinit1 で読み取りおよび書き込み操作中に割り込みからの保護なく使用されており、保護されていない可能性のあるグローバル変数であることを検出します。解析では、var4 の周期タスクの操作がオーバーフロー発生の原因になる可能性があることも示されます。保護されていない可能性のある変数およびオーバーフローを参照してください。

#include <assert.h>
#include "include/example_osek_multi.h"

int var1; 
int var2; 
int var3;

...
void func()
{
  var4++;
}

init によって var2 がインクリメントされた後 afterinit1 がアクティブ状態になる (ActivateTask()) ため、変数 var2 は共有されません。変数 var1 は、GetResource() 呼び出しおよび ReleaseResource() 呼び出しのクリティカル セクションで保護された変数です。

その他の考慮事項

• タスクを想定している関数またはマクロにパラメーターとしてタスクを渡す前に、DeclareTask または TASK キーワードを使用してすべてのタスクが宣言されていることを確認してください。たとえば、DeclareTask(foo); を使用せずにタスク foo を ActivateTask に渡した場合は、Polyspace がタスク foo を未定義と見なしてコンパイル エラーが発生します。

• 解析では、ソース コード内の TerminateTask() 宣言を無視し、それ以降のコードが実行されると見なします。

• Polyspace では、ここで定義された構文に従っていない OIL ファイルの構文要素を無視します。

• このオプションは、C コードを使用するプロジェクトに対してのみ使用できます。

依存関係

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

• オプション [ソース コードの言語] (-lang) の値を [C] に設定します。

• オプション [外部マルチタスキング構成] (Polyspace Platform ユーザー インターフェイスでは [マルチタスク用の外部ファイル] という名前に変更されます) で値 [osek] を選択します。

コマンド ライン情報

パラメーター: -osek-multitasking

値: auto | custom='file1 [,file2, dir1,...]'

既定値: オフ

例 (Bug Finder): polyspace-bug-finder -sources source_path -I include_path -osek-multitasking custom='path\to\file1.oil, path\to\dir'

例 (Code Prover): polyspace-code-prover -sources source_path -I include_path -osek-multitasking custom='path\to\file1.oil, path\to\dir'

例 (Bug Finder Server): polyspace-bug-finder-server -sources source_path -I include_path -osek-multitasking custom='path\to\file1.oil, path\to\dir'

例 (Code Prover Server): polyspace-code-prover-server -sources source_path -I include_path -osek-multitasking custom='path\to\file1.oil, path\to\dir'

バージョン履歴

R2017b で導入

参考

グローバル変数の共有と使用のみを表示 (-shared-variables-mode)

トピック

• Polyspace 解析オプションの指定
• Polyspace でのマルチタスキング プログラムの解析