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

[Frama-c-discuss] Problem with bitwise xor



Hollas Boris (CR/AEY1) wrote:
> In this code snippet, Jessie can't verify arithmetic overflow:
>
>
> typedef unsigned int uint32;
>
> uint32 Xor( uint32 x, uint32 y )
> {
>     return x ^ y;
> }
>
>
> This looks like a bug to me. I use Beryllium 1.
>
>   
Sorry for the dumb answer:  with which values of x and y do not you 
think there is an overflow ?

I don't even understand what arithmetic overflow may mean for xor.

Arithmetic overflow is a potential source of bugs with +, -, * and / 
that we try to prevent by default, because in general these operations 
should not overflow. It is just a matter of choice, because there is no 
corresponding runtime error.

Similarly, there is no possible runtime error in C for xor. What kind of 
general mistake could occur with xor ?

- Cladue


-- 
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                    |