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, чтобы Найти Дефекты от Определенных Системных Входных значений.

Смотрите также

|

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

Поддержка