--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on January 2010 ---
> 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. This needs to be recorded in a Bug Tracking System. The person in the best position to fix it just may not be reading the mailing list this week, or may be very busy with a deadline, or ... This may turn out to be a Why bug, but it's better to report this in the Frama-C BTS than not at all. It will be transmitted if it is. Regards, Pascal