--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on August 2018 ---
[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>