--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on November 2016 ---
Hello again, On 22/11/2016 09:38, Michael Tandy wrote: > 4. Why would I get a yellow circle on the signed overflow in a > statement as mundane as this? Have I misunderstood what the assertion > means, becuse it seems trivially true? > > uint8_t const * in = data_in; > /*@ assert rte: signed_overflow: (int)*in<<8 ⤠2147483647; */ > uint16_t msgType = (*in++)<<8; The exact cause of this unproven assertion is that WP by default does not establish a relation between the bitwise left shift and the arithmetic multiplication. You can, for instance, add a lemma stating that relation, as in the following example: #include <stdint.h> /*@ axiomatic ax { lemma mult256_lsl8: \forall integer x; (trigger: (x << 8)) == (x*256); } */ /*@ requires \valid_read(i); */ int main(uint8_t const *i) { uint16_t s = *i << ((uint8_t)8); return 0; } If you run this example with WP, it will then prove the assertion related to the unsigned overflow. But then you'll get another unproven property, which is the lemma itself. It can then be proved using an external prover such as Coq. There already exist some resources to help perform this proof in Coq, establishing relations between bitwise and arithmetic operations. Note that one of the reasons why such axioms are not included by default in WP is to avoid degrading proof performance. Including lots of such axioms could impact provers with potentially useless information, so the idea is that such axiomatics are added only when necessary. -- André Maroneze Ingénieur-chercheur CEA/LIST Laboratoire Sûreté et Sécurité des Logiciels -------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/pkcs7-signature Size: 3797 bytes Desc: S/MIME Cryptographic Signature URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20161122/cbbdb332/attachment.bin>