Polyspace 解析のグローバル変数範囲の制約

C/C++ コードのグローバル変数の範囲に外的制約 (データ範囲指定または DRS とも呼ばれます) を課し、変数への書き込み操作が制約に違反していないかどうかを Polyspace^® Code Prover™ でチェックできます。一般的なワークフローについては、Polyspace 解析の外的制約の指定を参照してください。

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

グローバル変数の範囲を制約し、制約への違反もチェックするには、次のようにします。

プロジェクト構成で、[入力およびスタブ] を選択します。[制約の設定] フィールドの横にあるボタンをクリックします。
[制約指定] ウィンドウで、をクリックします。
[Global Variables] ノードの下にグローバル変数のリストが表示されます。
制約するグローバル変数について、次のようにします。
- [グローバルアサート] 列のドロップダウンリストから、[Yes] を選択します。
- [グローバルアサート範囲] 列に範囲を min..max という形式で入力します。min はグローバル変数の最小値で、max は最大値です。
指定を保存するには、ボタンをクリックします。
[制約ファイルを保存] ウィンドウで、入力した内容を xml ファイルとして保存します。
検証を実行し、結果を開きます。
グローバル変数に対する書き込み操作ごとに、グリーン、オレンジまたはレッドの [正確性の条件] チェックが表示されます。チェックは次のようになります。
- グリーンの場合、変数は指定範囲内にあります。
- オレンジの場合、変数は指定範囲外にある可能性があります。
- レッドの場合、変数は指定範囲外にあります。
2 つ以上のタスクが同じグローバル変数に書き込むと、その変数が [グローバルアサート] 範囲外となる書き込み操作が 1 つのみである場合でも、その変数へのすべての書き込み操作で [正確性の条件] チェックがオレンジになります。

コマンドライン

オプション [制約の設定] (-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 ファイルで、グローバル変数を見つけて制約します。グローバル変数の XML タグは、file タグ内に直接現れ、function タグで囲まれていません。たとえば、次の制約 XML では、PowerLevel と SHR がグローバル変数です。

<file name="\\\\home\\johndoe\\Documents\\Polyspace_Workspace\\Examples\\Code_Prover_Example\\sources\\tasks1.c">
     <scalar name="PowerLevel" line="26" ... global_assert="YES" assert_range="0..10" />
     <scalar name="SHR" line="30" ... global_assert="NO" assert_range="" />
     <function name="Tserver" line="73" .../>
     <function name="initregulate" line="47" .../>
     <function name="orderregulate" line="35" ...>
           <scalar name="return" ... global_assert="unsupported" assert_range="unsupported" />
     </function>
     <function name="proc1" line="101" .../>
</file>

グローバル変数に対する制約を指定して、制約に違反しているかどうかを Code Prover 解析時にチェックするには、次のようにします。

変数の scalar タグの global_assert 属性を YES に設定します。
assert_range 属性に min..max の形式で 0..10 のように範囲を設定します。

前の例では、変数 PowerLevel がこのように制約されています。