Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>