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] Some newbie questions about frama-c

  • Subject: [Frama-c-discuss] Some newbie questions about frama-c
  • From: Andre.OLIVEIRAMARONEZE at cea.fr (Andre Maroneze)
  • Date: Tue, 22 Nov 2016 14:00:25 +0100
  • In-reply-to: <CAHGSkqjVKhG8Y74QkiL1WGsqgPXo_JjJHOgNkvu=iY7LD-DrpA@mail.gmail.com>
  • References: <CAHGSkqjVKhG8Y74QkiL1WGsqgPXo_JjJHOgNkvu=iY7LD-DrpA@mail.gmail.com>
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>