--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on October 2009 ---
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 |