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] How to deal with uint32
- Subject: [Frama-c-discuss] How to deal with uint32
- From: Claude.Marche at inria.fr (Claude Marche)
- Date: Mon, 26 Oct 2009 15:17:08 +0100
- In-reply-to: <4AE5A55F.3020307@adelard.com>
- References: <4AE5A55F.3020307@adelard.com>
Damien Karkinsky wrote: > Hi all, > > I have a problem with a piece of code that contains uint32 type defined > variables. When setting the variable, Frama-C attempts to prove that the > I guess you mean "the Jessie plugin of Frama-C attempts..." > value is within bounds and no overflow will occur. For example the code: > > uint32 Var1, Var2; > ... > Var1 |= ((Var1 ) & Var2); > > results in two proof obligations to show that; > 0<= bw_and(integer_of_uint32(Var1), integer_of_uint32(Var2)) > and > bw_and(integer_of_uint32(Var1), integer_of_uint32(Var2)) <= 4294967295 > > It seems the function integer_of_uint32 is undefined and hence the > The "hence" is not justified... There is an axiom somewhere that states forall x:uint32, 0 <= integer_of_uint32(Var2) <= 4294967295 so what is missing here is enough knowledge of the bitwise operator bw_and. You could try to add in your C file : /*@ lemma bw_and_uint32 : @ \forall uint32 x,y ; 0 <= x & y <= 4294967295; @*/ This lemma will not be proved, but will allow to prove your other VCs. The question of having a proper, sufficiently complete, axiomatization of bitwise operators in Jessie is open. We probably need to use built-in bitvector theories of SMT provers, but it is not done yet. - Claude > conditions cannot be discharged. Do you have any suggestions how to go > about this problem? > > Thank you > Regards > Damien > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |
- References:
- [Frama-c-discuss] How to deal with uint32
- From: dak at adelard.com (Damien Karkinsky)
- [Frama-c-discuss] How to deal with uint32
- Prev by Date: [Frama-c-discuss] How to deal with uint32
- Next by Date: No subject
- Previous by thread: [Frama-c-discuss] How to deal with uint32
- Next by thread: No subject
- Index(es):