Polyspace Code Prover でのオレンジ チェックの削減
オレンジ チェックは、Polyspace® が潜在的なランタイム エラーを検出したが、証明できないことを表します。Polyspace でより多くの証明された結果を生成するには、以下を実行可能です。
適切な検証オプションを指定する。
適切なコーディング方法に従う。
また、[結果のリスト] に表示されるオレンジ チェックの数とファミリを制限することもできます。詳細については、Limit Display of Orange Checks in Polyspace Platform User Interfaceを参照してください。
以下の 1 つ以上の操作を実行してオレンジ チェックを減らすことができます。
検証用のコンテキストを提供する
この例は、コードのランタイム実行に関する追加の情報を提供します。提供したコードがこれらの情報を含まない場合があります。次に例を示します。
main関数がない宣言済みであるが未定義の関数がある。
値が実行時にのみ使用可能な関数の引数がある。
特定の順序での実行を意図している関数を同時実行している。
十分な情報がない場合、Polyspace Code Prover™ はランタイム エラーが存在するか否かを検証できません。
オレンジ ソースの制約
比較的少数のオレンジ ソースを制約することによって、大部分のオレンジ チェックに対処できることがよくあります。
検証結果では、複数のオレンジ チェックの原因となる可能性がある volatile 変数やスタブ関数などのソースのリストを確認できます。このリストを表示するには、[結果の詳細] ペインで 
ボタンをクリックします。これらのソースを制約することによって、過大近似に由来するほとんどのオレンジ チェックを削除できます。長期的には、レビュー時にオレンジ ソースに対応して後の実行のためにこれらを制約するのではなく、最初の実行時にオレンジ ソースである可能性の高いソースを制約するための効率的な戦略を考案します。
オレンジ ソースのタイプとその制約方法については、オレンジ チェックの原因を参照してください。
一般的に使用されるコンテキストの仕様
検証のためにより多くのコンテキストを含めてオレンジ チェックを減らすには、以下の方法を利用します。
| 方法 | 例 |
|---|---|
Polyspace により生成された main が変数を初期化し、関数を呼び出す方法を定義する | Configure Library Verification |
| グローバル変数と関数の引数の範囲を定義する。 | Code Prover 解析結果からの制約テンプレートの作成 |
| マルチタスキングコードに実行順序を定義する。 | Polyspace マルチタスキング解析の手動設定 |
| 関数呼び出しサイトでの結果の精度を上げるため、解析精度が低い関数を標準関数にマップする。 | -code-behavior-specifications |
検証精度の向上
この例では、検証の精度を向上させる方法を説明します。精度を向上させることでオレンジ チェックは減少しますが、検証時間が増加します。
Polyspace Platform ユーザー インターフェイスでは、[実行時エラー] 、 [精度] の [静的解析] タブに表示されるオプションを使用します。
| オプション | 目的 |
|---|---|
精度レベル (-O0 | -O1 | -O2 | -O3) | 検証アルゴリズムを指定します。 |
検証レベル (-to) | ソース コードに対する Polyspace 検証プロセスの実行回数を指定します。 |
手続き間解析の精度を高める (-path-sensitivity-delta) | 関数の引数に関するより詳細な情報を、呼び出された関数に伝播します。 |
状況依存性 (-context-sensitivity) | 関数が 2 つの異なる呼び出しからの同じ命令でレッド チェックとグリーン チェックを含む場合、オレンジ チェックだけではなく両方のチェックが表示されます。 |
Polyspace Bug Finder を使用してコーディング ルールに従う
Polyspace Bug Finder™ を使用してコーディング ルールを適用すると、Polyspace Code Prover がランタイム エラーの有無を証明するのに役立ちます。コードが MISRA™ コーディング ルールの特定のサブセットに従う場合、Polyspace はより容易にランタイム エラーが存在するか否かを検証できます。
コードが MISRA コーディング ルールの関連するサブセットに従っているかどうかをチェックします。Polyspace Platform ユーザー インターフェイスでは、カスタム チェッカー ファイルを使用する場合にこれらのオプションを選択できます。プロジェクト構成を開き、[欠陥とコーディング規約] にある [静的解析] タブで、[カスタム チェッカー ファイルを使用] を選択します。次に、
アイコンを選択して [チェッカーの選択] ウィンドウを開き、以下のオプションを選択します。コードの種類 MISRA コーディング ルールを有効化するためのオプション サブセットの選択方法 手書きの C コード サイドバーから [MISRA C:2012] または [MISRA C:2023] を選択します。 ウィンドウの上部で、 SQO Level 1またはSQO Level 2を選択します。これらのサブセットの詳細については、MISRA コーディング規約のソフトウェア品質目標サブセットを参照してください。生成された C コード [MISRA AC AGC] ウィンドウの上部で、 SQO Level 1またはSQO Level 2を選択します。これらのサブセットの詳細については、MISRA コーディング規約のソフトウェア品質目標サブセットを参照してください。手書きの C++ コード [MISRA C++:2008] ウィンドウの上部で、 SQO Level 1またはSQO Level 2を選択します。これらのサブセットの詳細については、MISRA コーディング規約のソフトウェア品質目標サブセットを参照してください。[MISRA C++:2023] ウィンドウの上部で、ソフトウェア品質目標サブセット 1 を選択する場合は
MandatoryおよびRequiredを選択します。ソフトウェア品質目標サブセット 2 を選択する場合はAllを選択します。適切なソフトウェア品質目標サブセットを選択したら、Polyspace Bug Finder 解析を実行し、結果をレビューします。
コーディング ルール違反を修正します。
検証設定に関する提案への準拠
Polyspace Code Prover で、より適切な検証設定に関する提案が表示されることがあります。Code Prover では、検証の終了時に検証結果に対してアドバイザーが実行されます。アドバイザーは結果を照会し、検証時間の増加と精度の低下を引き起こす可能性がある問題を探します。アドバイザーは (組み込みルールに基づいて) 問題を検出すると、今後の実行でその問題を回避するために使用できる解析オプションを提案します。
次に例を示します。
生成した
mainが、既に他の場所で呼び出されている関数を多数呼び出す場合には、呼び出される関数の数を減らすことが提案されます。ほとんどのオレンジ チェックがグローバル変数に起因するものである場合には、これらのグローバル変数に対する制約を追加することが提案されます。
これらの提案は検証ログの終わりに表示されます。提案は次のように表示されます。
**********************************************************
***
*** Beginning Advisor
***
**********************************************************
Suggestion (polyspace.advisor.MainGeneratorCustomNeeded):
Issue: The generated main calls 54 functions, which might be too many and lead to loss of
performance and precision.
Cause: 49 functions are called both by the generated main and pointers to functions. These
functions are not unused and need not be called by the generated main.
Fix: Use -main-generator-calls custom=__bswap_16,__bswap_32,__bswap_64,apply_threshold,get_sum
**********************************************************
***
*** Advisor done
***
**********************************************************
修正の提案で Polyspace 解析オプションが言及されている場合、そのオプションをコピーして Polyspace オプション ファイルに貼り付けることができます。修正の提案に直接コピー可能なオプションが含まれていない場合でも、オレンジ チェック削減に向けて提案を使用することができます。
