--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on November 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Some newbie questions about frama-c



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>