Polyspace 解析の関数入力の制約

Polyspace^® Code Prover™ で解析されたプログラムモジュールに main 関数が含まれていない場合、既定では解析は実質上、呼び出されていないすべての関数から開始されます¹ .このような関数はコード内で呼び出されないため、Code Prover はそのデータ型に基づいて関数入力に関する仮定を行う必要があります。Code Prover 解析の精度を高めるために、これらの関数入力についての制約 (データ範囲指定 (DRS) とも呼ばれます) を指定できます。Code Prover では、これらの関数を解析して、制約された入力に関してランタイムエラーがないかを確認します。一般的なワークフローについては、Polyspace 解析の外的制約の指定を参照してください。

たとえば、次のように定義される関数では、引数 val の値が [1..10] の範囲にあるよう指定することができます。また、引数 ptr が指す 3 要素配列の各要素を初期化するように指定できます。

int func(int val, int* ptr) {
     .
     .
}

オプション [システムのすべての入力値を考慮する、さらに厳密なチェックを実行] (-checks-using-system-input-values) を使用する場合は、Bug Finder で関数入力に関する同様の仮定が表示されます。また、外的制約で Bug Finder 解析を制約することもできます。

関数がコード内で呼び出される場合、外的制約が適用されなくなることに注意してください。Code Prover はコード内のデータフローを追跡し、コード内で使用された実際の引数を使用して、呼び出された関数を解析します。

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

関数入力の制約を指定するには、次のようにします。

プロジェクト構成で、[入力およびスタブ] を選択します。[制約の設定] のボタンをクリックします。
[制約指定] ウィンドウで、をクリックします。
[User Defined Functions] ノードの下に、入力を制約できる関数のリストが表示されます。
各関数のノードを展開します。
各関数入力が個別の行に表示されます。入力には、function_name.arg1 や function_name.arg2 などの構文があります。
1 つ以上の関数入力に制約を指定します。詳細については、Polyspace 解析の外的制約を参照してください。
たとえば、前述のコードでは次のようにします。
- val を [1..10] の範囲に制約するには、[初期化モード] に [INIT] を選択し、[初期化範囲] で 1..10 を入力します。
- ptr の指定先として 3 要素配列の各要素が初期化されている場所を示すには、[初期化の割り当て] に [MULTI] を選択し、[割り当て可能オブジェクト数] で 3 を入力します。
検証を実行し、結果を開きます。[ソース] ペインで、カーソルを関数入力に置きます。
ツールヒントに制約が表示されます。たとえば、前述のコードの場合、ツールヒントには val の値が 1..10 であることが表示されます。

コマンドライン

オプション [制約の設定] (-data-range-specifications) を使用して、制約を指定する XML ファイルを指定します。

たとえば、Polyspace Code Prover Server™ による解析の場合、次のようにオプションを指定します。

polyspace-code-prover-server -sources filename -data-range-specifications "C:\Polyspace\drs_project1.xml"

Polyspace 解析の外的制約の指定の説明に従って、空白の制約 XML テンプレートを作成します。XML ファイルで、関数入力を見つけて制約します。関数入力は、function タグ内で scalar または pointer タグとして現れます。入力は arg1、arg2 などのように命名されます。たとえば、前のコードの場合、func の入力の XML 構造は次のようになります。

<function name="func" line="1" attributes="unused" main_generator_called="MAIN_GENERATOR" comment="">
     <scalar name="arg1" line="1" base_type="int32" complete_type="int32" init_mode="INIT" init_range="1..10" />
     <pointer name="arg2" line="1" complete_type="int32 *" init_mode="INIT" initialize_pointer="Not NULL" number_allocated="3" init_pointed="MULTI">  
         <scalar line="1" base_type="int32" complete_type="int32" init_mode="MAIN_GENERATOR" init_range=""/>
    </pointer>
     <scalar name="return" line="1" base_type="int32" complete_type="int32" init_mode="disabled" init_range="disabled"/>
</function>

関数入力に制約を指定するには、スカラー変数の場合、属性 init_mode および init_range を設定し、ポインター変数の場合、属性 init_pointed および number_allocated を設定します。

val を範囲 [1..10] に制約するには、arg1 という名前のタグの init_mode 属性を INIT に設定し、init_range を 1..10 に設定します。
ptr が指す 3 要素配列の各要素を初期化するように指定するには、arg2 という名前のタグの init_mode 属性を INIT、init_pointed を MULTI、および number_allocated を 3 にそれぞれ設定します。

参考

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

トピック

¹ The Code Prover analysis generates a main that calls all uncalled functions by default and starts analysis from this main. You can change this default behavior using the option Functions to call (-main-generator-calls) (Polyspace Code Prover).