--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on December 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Trouble With Why3 and New Frama-C 20.0



Thank you for the information. At least now I can stop tearing my hair
out.

On 12/19/2019 04:32 AM, Virgile Prevosto wrote:
> Hello,
>
> Thanks for the report. This is indeed a bug in the way WP handles boolean
> ACSL terms, and more specifically comparison operators returning a boolean
> when building a Why3 term with the Why3 API. Before it gets fixed, a work
> around is to stick with predicate, e.g.
> 
> /*@ predicate u8_continue_f(unsigned char b) =
>           0x80 <= b <= 0xBF;
> */
> 
> /*@
>         assigns \nothing;
>         ensures \result !=0 <==> u8_continue_f(b);
>         // or if you want to be more precise:
>         // ensures u8_continue_f(b) ==> \result ==1;
>         // ensures !u8_continue_f(b) ==> \result == 0;
>     */
>     int u8_is_continue(const unsigned char b)
>     {
>         return b >= 0x80 && b <= 0xBF;
>     }
> 
> Best regards,
> 
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>