Inputs in Polyspace Bug Finder

A Bug Finder analysis by default does not return a defect caused by a special value of an unknown input unless the input is subsequently bounded in the code. Polyspace makes no assumption about the value of unbounded inputs when your source code is incomplete. For example, in the following code Bug Finder detects a division by zero in foo_1(), but not in 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;	
}

To set bounds on your input, add constraints in your code such as assert or if. At the cost of a possibly longer runtime, you can perform a more exhaustive analysis where all values of function inputs are considered when showing defects. See Extend Bug Finder Checkers to Find Defects from Specific System Input Values.