--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on December 2009 ---
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 |