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

  • Subject: [Frama-c-discuss] Trouble With Why3 and New Frama-C 20.0
  • From: hirohito at cock.li (Emperor Hirohito)
  • Date: Thu, 19 Dec 2019 11:04:09 -0600
  • In-reply-to: <CA+yPOVhev9CvEBtwU=CbOs5vvNxqm-w0zTw51iujsawxXYj=4Q@mail.gmail.com>
  • References: <6034380f-ab86-3b04-736b-6814d15f8b25@cock.li> <CA+yPOVhev9CvEBtwU=CbOs5vvNxqm-w0zTw51iujsawxXYj=4Q@mail.gmail.com>
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
>