--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on July 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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