Code Prover のレッド チェックまたはオレンジ チェックの根本原因の特定

問題

検証後、操作がランタイム エラーの原因になるかどうかに応じて、コード内の操作が Polyspace^® Code Prover™ によって特定の色で強調表示されます。Code Prover の結果とソース コードの色を参照してください。

検証によって特定の操作がレッド (確実にランタイム エラーになる) またはオレンジ (ランタイム エラーになる可能性がある) で強調表示される理由が、ここですぐに判明するわけではありません。エラーの原因が分かったとしても、その修正方法がすぐに判明するとは限りません。

考えられる原因: 前のコード操作との関係

特定の操作でのランタイム エラーは、コード内の前の操作に関連することがよくあります。

たとえば、演算のオペランド値が大きくなるとオーバーフローしますが、このオペランドは前の演算での値を引き継いでいます。

解決法

前の操作が現在の操作でのランタイム エラーのきっかけになっているかどうかを調べるには、次を行います。

• 現在の操作の検証結果に関連付けられたメッセージを表示します。

  このメッセージは、[結果の詳細] ペインまたは [ソース] ペイン内でのその操作のツールヒントに表示されます。メッセージでは、結果をさらに詳しく調査する方法を示します。

  たとえば、以下のメッセージは、右側のオペランドがゼロになる可能性があることを示しています。どのようにすればオペランドの変数が値ゼロになるかを判断するには、これよりも前でこの変数に値を書き込んでいる操作を参照しなければなりません。

  

• コード内で現在の操作によりも前にあり、現在の操作に関連する操作を参照します。

  Polyspace ユーザー インターフェイスには、コード内の特定の位置へ簡単にナビゲーションできる機能があります。たとえば、関数名から関数定義に移動できます。

コード内で解決策を実装するのに適した場所を特定します。

各チェック タイプの確認方法についての詳細は、Code Prover の実行時チェックのレビューを参照してください。

考えられる原因: ソフトウェアの仮定

完全なアプリケーションを用意していない場合、または検証に必要な外部情報を提供していない場合、本ソフトウェアでは不足しているコードや外部情報について一定の仮定を行わなければなりません。

たとえば、main 関数を用意していない場合、呼び出されない関数のみを呼び出す main が本ソフトウェアでは生成されます。func1 が func2 を呼び出す場合、生成した main は func2 を再度呼び出しません。検証では、func1 の呼び出しコンテキストからのみ、func2 のランタイム エラーがチェックされます。

この仮定は、大部分のアプリケーションに当てはまるように行われます。ただし、ごく少数の場合に、既定の仮定がランタイム環境を正確に表していない場合があります。仮定が想定と異なる場合、予期しない検証結果になる可能性があります。

解決法

本ソフトウェアの仮定に対する検証結果をトレースできるかどうかを確認します。仮定の部分的なリストについては、Code Prover 解析の前提条件を参照してください。その他の仮定の一覧は、polyspaceroot\polyspace\verifier\code_prover_desktop の codeprover_limitations.pdf で提供されています。

多くの場合、特定のオプションを使用して既定の仮定を変更できます。

• ターゲットおよびコンパイラ:コンパイラの動作をエミュレートするためにオプションを設定しなければならないかどうか確認します。

  たとえば、除算演算の商を切り上げるのではなく切り捨てる場合、オプション除算での負方向への丸め (-div-round-down)を使用します。

• 入力およびスタブ:一部の変数を外部で制約しなければならないかどうかを確認します。

  たとえば、グローバル変数を特定の範囲内に制約する場合、オプション制約の設定 (-data-range-specifications)を使用します。

• マルチタスキング:一部のタスクや保護メカニズムの指定を忘れているかどうかを確認します。

  たとえば、関数が非プリエンプタブル割り込みを表すことを指定する場合は、オプション割り込み (-interrupts)を使用します。

• Code Prover 検証:main のないモジュールを検証している場合、生成された main がグローバル変数を初期化して関数を適切な順序で呼び出しているかどうかを確認します。

  たとえば、生成した main からすべての関数を呼び出す場合は、引数 all を指定したオプション呼び出す関数 (-main-generator-calls)を使用します。

• 検証の前提条件:検証のグローバルな前提条件がランタイム環境にとって適切かどうかを確認します。

  たとえば、不明なポインターが NULL 値になる可能性があると検証で見なす場合、オプション環境ポインターが安全でないことを考慮する (-stubbed-pointers-are-unsafe)を使用します。

• チェック動作:実行時チェックの指定がランタイム環境にとって適切かどうかを確認します。

  たとえば、不適切にデリファレンスされたポインターチェックで構造体のフィールド間でのポインター演算を許可する場合は、オプションフィールド間のポインター演算を有効にする (-allow-ptr-arith-on-struct)を使用します。

それでも結果を理解できない場合、結果の解釈を添えて MathWorks^® テクニカル サポートにお問い合わせください。実際の検証結果を共有できない場合は、その結果について不可欠な情報のみを提供してください。Polyspace 実行時の問題に関するテクニカル サポートへのお問い合わせを参照してください。