--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on July 2010 ---
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