--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on October 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to deal with uint32



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