--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on December 2019 ---
Hello, Le mer. 18 déc. 2019 à 19:10, Emperor Hirohito <hirohito at cock.li> a écrit : > I'm currently using Void Linux x86_64 5.4.2_1, if that's of any help. > > I have been messing around with Frama-C and wp for a little bit, but > the transition to Why3 has hit me with something odd that prevents me > from using wp. I've tried reinstalling using an essentially blank > slate (`rm -rf ~/.opam`), unless there are some residual configuration > files somewhere else. Here's the example file I'm using, just for > demonstration purposes: > > /*@ > logic boolean u8_continue_f(unsigned char b) = > 0x80 <= b <= 0xBF; > */ > /*@ > assigns \nothing; > ensures \result == (int)u8_continue_f(b); > */ > int u8_is_continue(const unsigned char b) > { > return b >= 0x80 && b <= 0xBF; > } > > 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, -- E tutto per oggi, a la prossima volta Virgile -------------- section suivante -------------- Une pièce jointe HTML a été nettoyée... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20191219/1d9b893e/attachment.html>