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 を指定します。解析後、空白のテンプレート XML drs-template.xml が結果フォルダーに作成されます。
C++ プロジェクトで空白の制約テンプレートを作成するには、オプション [検証レベル] (-to) に引数 cpp-normalize を使用する必要があります。
XML ファイルを編集して制約を指定します。
以下の例を参照してください。
- Polyspace 解析のグローバル変数範囲の制約
- Polyspace 解析の関数入力の制約

Code Prover 解析結果からの制約テンプレートの作成

実際のアプリケーションの想定範囲に基づいて変数範囲を制約できます。たとえば、変数が車両の速度を表す場合、取り得る最大値を設定できます。また、変数範囲が原因で、過大近似によりオレンジチェックが大量になる場合のみ、変数範囲を制約することもできます。

Code Prover 解析では、想定される過大近似によりオレンジチェックにつながる、すべてのグローバル変数、関数入力、およびスタブ関数が表示されます。解析精度を上げるために、これらの変数のみを制約することができます。

Polyspace ユーザーインターフェイスまたは Polyspace Access Web インターフェイスで Code Prover の結果を開きます。
[オレンジソース] ペインを開きます。次のいずれかを行います。
- オレンジチェックを選択します。ソフトウェアがオレンジチェックを根本原因までトレースできる場合、アイコンが [結果の詳細] ペインに表示されます。このアイコンをクリックして [オレンジソース] ペインを開きます。
- Polyspace ユーザーインターフェイスで、[ウィンドウ] 、 [ビューの表示/非表示] 、 [オレンジソース] を選択します。Polyspace Access Web インターフェイスで、[ウィンドウ] 、 [オレンジソース] を選択します。
オレンジチェックの原因となる可能性のある変数 (関数の入力またはスタブ関数の戻り値) の完全なリストが表示されます。これらの変数の範囲を制約します。

個別のオレンジチェックの詳細では、次のようなメッセージが頻繁に表示されます。

適切な場合、example.c の 44 行目にあるスタブ関数 random_float に DRS を適用すると、このオレンジ表記が解消するかもしれません。

このメッセージは、スタブ関数がオレンジチェックの原因である可能性を示しています。関数に外部制約を適用することにより、より正確な仮定を実行し、場合によってはオレンジチェックの解消が可能です (仮定の範囲の広さが原因である場合)。

既存のテンプレートの更新

新しいコード送信では、追加の制約を指定しなければならない場合があります。既存のテンプレートを更新して、新しいコード送信に由来するグローバル変数、関数入力、およびスタブ関数を追加できます。

また、コードから一部の変数や関数を削除すると、それらに対する制約が適用されなくなります。制約テンプレートの生成や制約の指定を再度実行する代わりに、既存のテンプレートを更新してコードにない変数を削除できます。

ユーザーインターフェイス (デスクトップ製品のみ)

[構成] ペインで、[入力およびスタブ] を選択します。
以下のいずれかの方法で既存のテンプレートを開きます。
- [制約の設定] フィールドにテンプレート XML ファイルへのパスを入力します。[編集] をクリックします
- [編集] をクリックします[制約指定] ダイアログボックスでアイコンをクリックして、テンプレートファイルに移動します。
[更新] をクリックします。
1. ソースコードに存在しない変数は [Non Applicable] ノードに表示されます。[Non Applicable] ノードに表示されたエントリまたはノード自体を削除するには、右クリックして [このノードを削除] を選択します。
2. その他の変数に対して新しい制約を指定します。

コマンドライン

継続的インテグレーションワークフローでは、前回の実行の制約 XML ファイルを使用できます。新しいコード送信により、追加の制約が必要な場合、次のようにします。

新しいコード送信の変数に対する制約を制約 XML ファイルに指定します。次を参照してください。制約テンプレートの作成:コマンドライン
新しい制約を含む制約 XML ファイルを前回の実行の制約 XML ファイルとマージします。

コードでの制約の指定

コードの外部で制約を指定すると、解析の正確性が向上します。ただし、制約がコードの "外部" にあるため、指定された制約内でコードを使用しなければなりません。そうでない場合、結果が適用されない可能性があります。たとえば、指定された範囲外の関数入力を使用する場合、演算のチェックがグリーンであってもランタイムエラーが発生する可能性があります。

コードの "内部" で制約を指定するために、以下を使用することができます。

コードの適切なエラー処理テスト。
Polyspace のチェックでエラーが実際に発生するかどうかが判定されます。エラーが発生しない場合、テストブロックが [到達不能コード] として表示されます。
unchecked_assert マクロ。たとえば、変数 var を範囲 [0,10] 内に制約するには、assert(var >= 0 && var <=10); を使用できます。
手動スタブと手動の main() 関数を使用した Polyspace 解析の変数範囲の制約を参照してください。

参考

制約の設定 (-data-range-specifications)