--- layout: fc_discuss_archives title: Message 58 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



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                    |