このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。
マルチタスクを手動で構成
コードがマルチタスキングを対象としていることの考慮
説明
コードがマルチタスク アプリケーションかどうかを指定します。このオプションにより、Polyspace® のマルチタスク構造を手動で構成できるようになります。
オプションの設定
以下のいずれかの方法を使用してオプションを設定します。
Polyspace ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [マルチタスキング] ノードを選択してから、このオプションを選択します。
Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [マルチタスキング] ノードを選択してから、このオプションを選択します。
コマンド ラインとオプション ファイル: コマンド ライン情報を参照してください。
このオプションを使用する理由
既定では、Bug Finder により、使用しているマルチスレッド関数からマルチタスキング モデルが判断されます。Code Prover では、オプション [Code Prover の同時実行の自動検出を有効にする] (-enable-concurrency-detection) を使用して、同時実行の自動検出を有効にする必要があります。ただし、場合によっては、同時実行の自動検出を使用すると、Code Prover 解析の速度が低下する可能性があります。
同時実行の自動検出がサポートされていない場合は、このオプションを使用してマルチタスキング モデルを明示的に指定できます。このオプションを選択すると、エントリ ポイント関数、周期タスク、割り込み、およびクリティカル セクション詳細などの共有変数の保護メカニズムを明示的に指定できます。
Code Prover 検証では、この指定を使用して以下が判断されます。
グローバル変数が共有されているかどうか。
グローバル変数を参照してください。
ランタイム エラーが発生する可能性があるかどうか。
たとえば、演算
var++が周期タスクの本体内で行われ、varに制限を設けていない場合、この演算はオーバーフローする可能性があります。解析により、オーバーフローが発生する可能性が検出されます。
Bug Finder 解析では、この指定を使用して、同時実行の欠陥が調査されます。詳細は、同時実行の欠陥を参照してください。
設定
オンコードはマルチタスキング アプリケーションを対象とします。
他の Polyspace オプションを使用して、マルチタスキング構成を明示的に指定する必要があります。Polyspace マルチタスキング解析の手動設定を参照してください。
オフ (既定の設定)コードはマルチタスキング アプリケーションを対象としません。
このオプションを無効にすると、Code Prover では次のような付加的な影響が生じます。
mainが存在する場合、Code Prover はmainから呼び出される関数のみを検証します。mainが存在しない場合、Polyspace は指定された関数を検証します。それらの関数を検証するために、Polyspace はmain関数を生成し、生成されたmainから関数を指定の順序で呼び出します。詳細は、モジュールまたはライブラリの検証 (-main-generator)を参照してください。
ヒント
Code Prover でファイルごとの検証を実行する場合、マルチタスキング オプションは無視されます。ファイルを個別に検証 (-unit-by-unit) を参照してください。
コマンド ライン情報
マルチタスキング解析をオンにする単一のコマンド ライン オプションはありません。オプション [タスク] (-entry-points)、[周期タスク] (-cyclic-tasks)、または [割り込み] (-interrupts) のいずれかを使用して、マルチタスキング解析をオンにします。
