--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on January 2010 ---
Hello, Consider the following: bool_t func1(float32_t x); /*@ ensures \result == TRUE */ bool_t func1(float32_t x) { if (x < 1E-6) { ; } return TRUE; } Alt-Ergo and CVC3 claim a syntax error on the input from Frama-C. I think its the constant expression 1E-6 that causes the problem. Are there any ways around this? Regards Damien