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

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                    |