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



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>