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] Type casts and wp

Hello,

Le ven. 24 août 2018 à 21:54, Sebastian Götte <jaseg at physik.tu-berlin.de> a
écrit :

> Hi,
>
> I'm a grad student of computer science currently playing around with
> frama-c in their spare time and I've struck one case where I don't
> understand the behavior of frama-c/wp. Given the following program
> frama-c/wp cannot prove the assert c_gt_0. Everything else is proven
> successfully.  Intuitively it seems to me that from x >= 0 and x != 0
> follows x > 0, and indeed for d that is the case, but not for c. I would
> like to understand why that is so.
>
>      size_t test(char foo, unsigned int d) {
>          unsigned int c = (unsigned char)foo;
>          if (c != 0) {
>              //@ assert   c_gt_0: c > 0;
>              return c + d;
>          }
>

The subject of your email is on the right track: the conversion from
(signed, as is the case for the default architecture considered by Frama-C)
char to unsigned char is getting on the way. More specifically, in the
logic formulas given to the provers, c is seen as to_uint8(i)  the
conversion of an unspecified integer i into an 8-bit unsigned. There are
two axioms in WP's arithmetic model that are sufficient to prove your goal,
namely is_to_uint8, stating that the result of to_uint8 is a uint8, and
is_uint8_def, stating that a uint8 is within 0 and 255. Unfortunately,
Alt-Ergo does not instantiate the former automatically (the trigger given
by WP might need to be refined, but finding appropriate triggers is a very
delicate balance). However, if you instantiate is_to_uint8 manually in
Altgr-ergo GUI (launched from Frama-C's GUI if you double-click on the
Alt-Ergo column in the line of the corresponding goal in the WP Goals tab),
the rest of the proof is immediate.

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/20180827/f21ffdf1/attachment.html>