--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on December 2009 ---
> 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. Jesse generates VC for arithmetic overflow and can't prove them. You are right that with bitwise operations, no overflow can occur. Still Jessie tries to verify sth and fails. Hence, I don't get green bullets for this code. I filed bug report http://bts.frama-c.com/view.php?id=348 on this. -Boris