Exponenta Banner

Входы в Polyspace Bug Finder

Анализ Bug Finder по умолчанию не возвращает дефект, вызванный специальным значением неизвестного входного сигнала, если вход не ограничен. Polyspace не делает никаких предположений о значении неограниченных входов, когда ваш исходный код неполен. Например, в следующем коде Bug Finder обнаруживает division by zero в 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 Checkers для поиска дефектов из значений Входа конкретной системы».

См. также

|

Документация Polyspace Bug Finder

Поддержка