Polyspace 解析の外的制約の指定
Polyspace® 製品は C/C++ コードを解析して欠陥 (バグ) やランタイム エラーなどの問題をチェックします。解析では指定されたコードを使用して、変数の範囲やポインターに許容されるバッファー サイズなどの項目について仮定を行います。仮定は予想よりも幅広くなる場合があります。その理由は次のとおりです。
完全なコードが提供されていない。たとえば、関数定義の一部が提供されなかった場合。
変数に関する一部の情報が実行時にのみ利用可能である。たとえば、コード内の一部の変数が実行時にユーザーから値を取得する場合。
このように仮定の幅が広いため、以下のようになります。
Code Prover では実行時に発生するパスよりも多くの実行パスを考慮する可能性があります。実行パスの 1 つで操作が失敗すると、Polyspace はこの操作に対してオレンジ チェックを付けます。その実行パスが、あまりにも広範に及ぶ仮定に由来する場合、オレンジ チェックは誤検知を示すことがあります。
Bug Finder では誤検知が生じることがあります。
こうした誤検知の数を減らすには、グローバル変数、関数入力、およびスタブ関数の戻り値と変更可能な引数についての追加的な制約を指定します。この例では、それらの外的制約 (データ範囲指定 (DRS) とも呼ばれる) を指定する方法を示します。以降の解析で使用するために制約を XML ファイルとして保存します。ソース コードを変更する場合、以前の制約を更新できます。制約テンプレートを新規に作成する必要はありません。
制約テンプレートの作成
ユーザー インターフェイス (デスクトップ製品のみ)
プロジェクト構成を開きます。[構成] ペインで、[入力およびスタブ] を選択します。
[制約の設定] の右にある [編集] ボタンをクリックして [制約指定] ウィンドウを開きます。
[制約指定] ダイアログ ボックスで、空白の制約テンプレートを作成します。テンプレートにはすべての変数リストが含まれており、そこで制約を指定できます。新しいテンプレートを作成するために
をクリックします。ソフトウェアはプロジェクトをコンパイルし、テンプレートを作成します。新しいテンプレートは、プロジェクト フォルダーのファイル Module_number_Project_name_drs_template.xml制約を指定し、XML ファイルとしてテンプレートを保存します。詳細については、Polyspace 解析の外的制約を参照してください。
[OK] をクリックします。
テンプレートの XML ファイルの絶対パスが [制約の設定] フィールドに表示されます。解析を実行すると、Polyspace は変数の制約を抽出する際にこのテンプレートを使用します。
コマンド ライン
オプション [制約の設定] (-data-range-specifications) を使用して、制約 XML ファイルを指定します。
XML ファイルに制約を指定するには、次のようにします。
まず、空白の XML テンプレートを作成します。テンプレートには、制約の指定なしでグローバル変数、関数入力、およびスタブ関数の変更可能な引数と戻り値がすべてリストされます。
空白のテンプレートを作成するには、コンパイル段階までに限り解析を実行します。Bug Finder で、欠陥のチェックを無効にします。オプション
[欠陥の検出] (-checkers)を使用します。Code Prover で、ソース準拠のみをチェックします。オプション[検証レベル] (-to)に引数compileを指定します。解析後、空白のテンプレート XMLdrs-template.xmlが結果フォルダーに作成されます。C++ プロジェクトで空白の制約テンプレートを作成するには、オプション
[検証レベル] (-to)に引数cpp-normalizeを使用する必要があります。XML ファイルを編集して制約を指定します。
以下の例を参照してください。
Code Prover 解析結果からの制約テンプレートの作成
実際のアプリケーションの想定範囲に基づいて変数範囲を制約できます。たとえば、変数が車両の速度を表す場合、取り得る最大値を設定できます。また、変数範囲が原因で、過大近似によりオレンジ チェックが大量になる場合のみ、変数範囲を制約することもできます。
Code Prover 解析では、想定される過大近似によりオレンジ チェックにつながる、すべてのグローバル変数、関数入力、およびスタブ関数が表示されます。解析精度を上げるために、これらの変数のみを制約することができます。
Polyspace ユーザー インターフェイスまたは Polyspace Access Web インターフェイスで Code Prover の結果を開きます。
[オレンジ ソース] ペインを開きます。次のいずれかを行います。
オレンジ チェックを選択します。ソフトウェアがオレンジ チェックを根本原因までトレースできる場合、
アイコンが [結果の詳細] ペインに表示されます。このアイコンをクリックして [オレンジ ソース] ペインを開きます。Polyspace ユーザー インターフェイスで、[ウィンドウ] 、 [ビューの表示/非表示] 、 [オレンジ ソース] を選択します。Polyspace Access Web インターフェイスで、[ウィンドウ] 、 [オレンジ ソース] を選択します。
オレンジ チェックの原因となる可能性のある変数 (関数の入力またはスタブ関数の戻り値) の完全なリストが表示されます。これらの変数の範囲を制約します。
個別のオレンジ チェックの詳細では、次のようなメッセージが頻繁に表示されます。
適切な場合、example.c の 44 行目にあるスタブ関数 random_float に DRS を適用すると、このオレンジ表記が解消するかもしれません。
このメッセージは、スタブ関数がオレンジ チェックの原因である可能性を示しています。関数に外部制約を適用することにより、より正確な仮定を実行し、場合によってはオレンジ チェックの解消が可能です (仮定の範囲の広さが原因である場合)。
既存のテンプレートの更新
新しいコード送信では、追加の制約を指定しなければならない場合があります。既存のテンプレートを更新して、新しいコード送信に由来するグローバル変数、関数入力、およびスタブ関数を追加できます。
また、コードから一部の変数や関数を削除すると、それらに対する制約が適用されなくなります。制約テンプレートの生成や制約の指定を再度実行する代わりに、既存のテンプレートを更新してコードにない変数を削除できます。
ユーザー インターフェイス (デスクトップ製品のみ)
[構成] ペインで、[入力およびスタブ] を選択します。
以下のいずれかの方法で既存のテンプレートを開きます。
[制約の設定] フィールドにテンプレート XML ファイルへのパスを入力します。[編集] をクリックします
[編集] をクリックします[制約指定] ダイアログ ボックスで
アイコンをクリックして、テンプレート ファイルに移動します。
[更新] をクリックします。
ソース コードに存在しない変数は [Non Applicable] ノードに表示されます。[Non Applicable] ノードに表示されたエントリまたはノード自体を削除するには、右クリックして [このノードを削除] を選択します。
その他の変数に対して新しい制約を指定します。
コマンド ライン
継続的インテグレーション ワークフローでは、前回の実行の制約 XML ファイルを使用できます。新しいコード送信により、追加の制約が必要な場合、次のようにします。
新しいコード送信の変数に対する制約を制約 XML ファイルに指定します。次を参照してください。制約テンプレートの作成:コマンド ライン
新しい制約を含む制約 XML ファイルを前回の実行の制約 XML ファイルとマージします。
コードでの制約の指定
コードの外部で制約を指定すると、解析の正確性が向上します。ただし、制約がコードの "外部" にあるため、指定された制約内でコードを使用しなければなりません。そうでない場合、結果が適用されない可能性があります。たとえば、指定された範囲外の関数入力を使用する場合、演算のチェックがグリーンであってもランタイム エラーが発生する可能性があります。
コードの "内部" で制約を指定するために、以下を使用することができます。
コードの適切なエラー処理テスト。
Polyspace のチェックでエラーが実際に発生するかどうかが判定されます。エラーが発生しない場合、テスト ブロックが [到達不能コード] として表示されます。
unchecked_assertマクロ。たとえば、変数varを範囲 [0,10] 内に制約するには、assert(var >= 0 && var <=10);を使用できます。
参考
制約の設定 (-data-range-specifications)
