Polyspace Bug Finder における入力

Bug Finder 解析は、既定で、コード内で以降の入力が制限されていない限り、不明な入力の特殊な値によって発生した欠陥を返しません。ソース コードが不完全な場合、Polyspace では制限されていない入力の値に関する仮定を行いません。たとえば、次のコードで Bug Finder は [ゼロ除算] を foo_1() で検出しますが、foo_2() では検出しません。

int foo_1(int p) 
{ 
  int x = 0; 
  if ( p > -10 && p < 10 )  /* p is bounded by if statement */
	  x = 100/p;	/* Division by zero detected */
	  
  return x; 
} 

int foo_2(int p)	/* p is unbounded */ 
{ 
  int x = 0; 
  x = 100/p;	/* Division by zero not detected */
  

  return x;	
}

入力に制限を設定するには、コードに assert や if などの制約を追加します。ランタイムは長くなりますが、欠陥を表示するときに関数入力のすべての値が考慮されるより徹底的な解析を実行できます。特定のシステム入力値から欠陥を見つけるための Bug Finder チェッカーの拡張を参照してください。

参考

|