// Problem: The frama-c is giving 'crash' while slicing
// Frama-C command to run: frama-c -slice-print -slice-pragma f2 frama-c_crash_float_param.c
int  glb_int;
float  glb_float;
 
int f2 (int param_int, float param_float ) {
	//@slice pragma stmt;
   if ( param_float == 32 && param_int == 31 );  // for this stmt, there is crash

   /* Below are the some of the observations...
   if ( param_float == 32 && param_int == 31 );  // for this stmt, there is crash
   if ( param_int == 32 && param_float == 31 );  // for this stmt, there is NO crash
   if ( param_float == 32 || param_int == 31 );  // for this stmt, there is NO crash
   if ( param_float > 32 && param_int == 31 );  // for this stmt, there is NO crash
   if ( param_float == 32);		  // for this stmt, there is NO crash
   */
}

int main( ) { 
	inputsOf_ff_f2( );
	f2 ( glb_int,  glb_float);
}

int nondet_int ( );
float nondet_float ( );
void inputsOf_ff_f2 () {
	glb_int = nondet_int ( );
	glb_float = nondet_float ( );
}