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