Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Floating-point NaN Detection

  • Subject: [Frama-c-discuss] Floating-point NaN Detection
  • From: eric.liu at uniquesoft.com (Eric Liu)
  • Date: Tue, 13 Jul 2010 12:56:03 +0800
Hi, frama-c folks:

I am testing if frama-c can detect NaN. Here is my test code.

void NaN(int c[])
{
	double * p = NULL;
	p = c;
	printf("integer c[0] = %u, c[1] = %d --> double %f\n", c[0], c[1], *p);
}

int main(int argc, char * argv[])
{
	int c[2] = {argc, argc};
	NaN(c);
	return 0;
}

I have read the user manual. It says it can detect possible NaN in
"double" type only. When I run my test with command line "frama-c -val
myfile.c", frama-c does not produce any warning message at all. Help,
please!

By the way, I also test infinite value. It works fine.

My frama-c is Boron-20100401.

Thanks
Eric