--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on October 2009 ---
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 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 conditions cannot be discharged. Do you have any suggestions how to go about this problem? Thank you Regards Damien