Polyspace Code Prover での重要なオレンジチェック

Code Prover は、特定の種類のランタイムエラーについてコードを網羅的にチェックします。チェックが確定的ではない場合、結果はオレンジ色 (疑問符付き) で表示されます。各オレンジチェックに関して解析から提供される追加情報は、チェックが潜在的なランタイムエラーを表しているのか、あるいは過大近似または広範な仮定の結果を表しているのかを判断する上で役立ちます。

List of critical orange checks in Code Prover.

ランタイムエラーである可能性が高いチェックは、重要なオレンジチェックと見なされます。レッドチェックとグレーチェックは、その定義上、クリティカルなチェックの範囲に含まれます。これは、レッドチェックが明確なランタイムエラーを示し、グレーチェックは (現在の検証の前提条件下では) 明らかに到達不能なコードを示すためです。通常、レッドチェックとグレーチェックで示されるエラーは明確なエラーです。オレンジチェックの場合、重要なチェックを確認することで、ランタイムエラーの可能性が高い結果のレビューに集中できます。

重要なチェックのみを表示する方法

Code Prover の結果リストを、レッドチェック、グレーチェック、および重要なオレンジチェックのみに絞り込むことができます。

Polyspace Access Web インターフェイスおよび Polyspace Platform ユーザーインターフェイス

Polyspace^® Access™ Web インターフェイスと Polyspace Platform ユーザーインターフェイスでは、個別のフィルターを使用してレッドチェック、グレーチェック、重要なオレンジチェックに絞り込むことができます。

色別のフィルターを使用して、レッドチェック、グレーチェック、オレンジチェックのみを表示します。
ツールストリップにある [スポットライトフィルター] を使用すると、潜在的なランタイムエラーをより効率的にレビューできます。次のフィルターがあります。
- オレンジソース — オレンジソースに関連するオレンジの結果をリストします。
- 重要なチェック — ランタイムエラーになる可能性が高いオレンジの結果をリストします。
テキストベースのフィルターを使用して、重要なオレンジチェックのみを表示します。[表示のみ] テキストフィルターに、パス関連のオレンジチェックを表示する場合は [出発点:パス関連の問題] と入力し、限定的な入力値に関連するオレンジチェックを表示する場合は [出発点:制限付き入力] と入力します。

Polyspace デスクトップユーザーインターフェイス

Polyspace デスクトップ製品のユーザーインターフェイスでは、結果リストを重要なチェックのみに直接絞り込むことができます。[結果のリスト] ペインの [すべての結果] ドロップダウンから [Critical checks] を選択します。

Dropdown showing critical checks

[Critical checks] を選択すると、[結果のリスト] ペインにレッドチェック、グレーチェック、重要なオレンジチェックのみが表示されます。

重要と見なされるオレンジチェック

重要なチェックという概念により、オレンジチェックのレビューに優先順位を指定できます。重要なオレンジチェックを他のオレンジチェックよりも先にレビューするか、または重要なオレンジチェックのみをレビューすることを選択できます。Polyspace Code Prover でのオレンジチェックの管理も参照してください。

重要なオレンジチェックは、"パス" と "限定的な入力値" に関連しています。ここでは、入力値とはアプリケーションの外部にある値のことです。たとえば、以下のようなものがあります。

生成された main によって呼び出される関数への入力。生成された main によって呼び出される関数の詳細は、呼び出す関数 (-main-generator-calls)を参照。
グローバル変数および volatile 変数。
スタブ関数によって返されるデータ。データは関数またはポインターによって変化する関数パラメーターによって返される値である。

チェックがパス関連なのか入力値関連なのかについて、ソフトウェアが判別できないというオレンジチェックが発生する可能性があることに注意してください。したがって安全対策として、まず重要なチェックをレビューしてから他のチェックをレビューしてください。ただし、重要なチェックしかレビューしないということのないようにしてください。

パス

パス関連のチェックは重要なオレンジチェックの範囲に含まれます。[結果のリスト] ペインでは、このようなチェックの [情報] 列には [出発点:パス関連の問題] というフィルターを選択します。ランタイムエラーが発生する可能性がある明確な実行パスがソフトウェアによって識別されたため、これらのチェックは重要です。この実行パスは明確であり、このチェックの行で終わるその他のパスから分離可能です。これは、コード内の異なる複数の命令を通過するためです (命令は同じでも異なる入力値で通過する可能性もあります)。

次の例では、パス関連のオレンジチェックを示します。

void path(int x) { 
   int result; 
   result = 1 / (x - 10); 
   // Orange division by zero
 } 

void main() { 
    path(1);
    path(10);
 }

オレンジの [ゼロ除算] チェックが潜在的なエラーとして識別されています。[結果の詳細] ペインは、次のように潜在的なエラーを示します。

...
Warning: scalar division by zero may occur
...

この result=1/(x-10) の [ゼロ除算] チェックは、次の理由によりオレンジになっています。

path(1) はゼロ除算エラーを発生させない。
path(10) はゼロ除算エラーを発生させる。

この場合のオレンジチェックは、明確なランタイムエラーを表していることに注意してください。したがってこの解析は、パス関連のオレンジチェックの他に、path(10) の [無限呼び出し] レッドエラーによるエラーも示します。

限定的な入力値

限定的な入力値に関連するチェックは、重要なオレンジチェックの範囲に含まれます。[結果のリスト] ペインでは、このようなチェックの [情報] 列には [出発点:制限付き入力] というエントリが表示されます。外部で制限されている一部のプログラム入力でランタイムエラーが発生する可能性があることを、ソフトウェアが識別したため、これらのチェックは重要です。入力値が明示的に限定されているため、ソフトウェアで入力に関する仮定を行う必要はありませんでした。したがって、入力値とそれに伴うランタイムエラーが実際に発生する可能性があります。

大半の入力値は外的制約 (データ範囲指定 (DRS) とも呼ばれる) によって限定されます。入力およびスタブも参照してください。

次の例では、限定的な入力値に関連するオレンジチェックを示します。

int tab[10]; 
extern int val; 
// You specify that val is in [5..10]
 
void assignElement(int index) { 
   int result; 
   result = tab[index];  
   // Orange Out of bounds array index
 } 
void main(void) {
   assignElement(val); 
}

変数 val に対して 5 ～ 10 の範囲の PERMANENT データを指定すると、tab[index] に対して [範囲外の配列インデックス] オレンジチェックが検証により生成されます。[結果の詳細] ペインでは、以下のように潜在的なエラーの詳細が提供され、チェックが限定的な入力値に関連している可能性があることが示されます。

Warning: array index may be outside bounds: [0..9]
This check may be an issue related to bounded input values
Verifying DRS on extern variable val may remove this orange. 
  array size: 10 
  array index value: [5 .. 10]

制限されていない入力値

制限されていない入力値に関連するチェックは、重要なオレンジチェックの範囲に含まれません。[結果のリスト] ペインでは、このようなチェックの [情報] 列には [出発点:入力による影響の可能性] エントリが表示されます。制限されていない一部のプログラム入力でランタイムエラーが発生する可能性があることが識別されたため、これらのチェックは重要なチェックとして見なされません。入力値が制限されていないため、入力データ型に基づいてさまざまな入力値が想定されます。入力値とそれに伴なうランタイムエラーは、実際には発生しない可能性があります。

次の例では、潜在的なランタイムエラーとして識別される可能性のある制限されていない入力値に関連するオレンジチェックを示します。

int tab[10]; 
extern int val; 
 
void assignElement(int index) { 
   int result; 
   result = tab[index];  
   // Orange Out of bounds array index
 } 
void main(void) {
   assignElement(val); 
}

tab[index] に対してオレンジの [範囲外の配列インデックス] チェックが検証で生成されます。[結果の詳細] ペインでは、以下のように潜在的なエラーの詳細が提供され、制限されていない入力値にチェックが関連している可能性があることが示されます。

Warning: array index may be outside bounds: [0..9]
This check may be an issue related to unbounded input values
If appropriate, applying DRS to extern variable val may remove this orange. 
 array size: 10 
 array index value: [-2³¹ .. 2³¹-1]