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

[Frama-c-discuss] bug with output to Alt-Ergo and CVC3



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