マルチタスキング チェックの構成
エントリ ポイント、割り込み、周期タスク、時間的に排他なタスクなど、コードで使用するマルチタスキング構成要素を指定する
Polyspace® では、POSIX® ライブラリや C11 および C++11 の標準ライブラリなど、複数のマルチタスキング ライブラリが既定でサポートされています。サポートされているマルチタスキング ライブラリとキーワードの一覧については、Polyspace でのスレッド作成とクリティカル セクションの自動検出を参照してください。
別のマルチタスキング ライブラリを使用する場合は、オプション -code-behavior-specifications を使用して、使用するライブラリをサポートされているライブラリにマッピングします。
または、ここに記載しているオプションを使用して、コード内でエントリ ポイント、周期タスク、または割り込みを示す関数を指定します。また、共有変数の保護メカニズムも指定しなければなりません。
Polyspace オプション
トピック
- Polyspace でのマルチタスキング プログラムの解析
Bug Finder でデータ レースやデッドロックを検出、または Code Prover で共有変数の使用の包括的な解析を確認します。
- マルチタスキング コードでの共有変数の保護
クリティカル セクション、時間的に排他、優先順位、または割り込みの無効を使用して共有変数を保護する。
- Polyspace でのデータ レース検出のタスク優先順位の定義
タスクを非プリエンプタブルにし、割り込みをプリエンプタブルにすることで、タスクの優先順位をエミュレートする。
関連情報
- グローバル変数 (Polyspace Code Prover)
