--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on December 2019 ---
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 >