--- layout: fc_discuss_archives title: Message 15 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



> 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