--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on November 2013 ---
Hi, It reminds me a overflow proof obligation generated by jessie for bitwise-and operation: if ( TRAP_DEBUG_ENABLE == (Sys_health & TRAP_DEBUG_ENABLE) ) { // where the macro and variable are defined as: // unsigned int Sys_health=0; // #define TRAP_DEBUG_ENABLE (unsigned int) (0x80000000) } And the auto-provers are unable to prove Sys_health & TRAP_DEBUG_ENABLE does not overflow. Is this perhaps the same issue? cheers xiaolei > Date: Fri, 8 Nov 2013 04:48:20 +0100 > From: guillaume.melquiond at inria.fr > To: frama-c-discuss at lists.gforge.inria.fr > Subject: Re: [Frama-c-discuss] math vs. bits > > On 08/11/2013 04:25, John Regehr wrote: > > The functions below have identical specifications and are functionally > > equivalent. All provers (Z3, Yices, CVC4) were able to verify all VCs > > for the first one, yet the second had a number of VCs that no prover > > could discharge. > > > > I'm curious if this might be some sort of bug in Jessie or Frama-C, or > > are our provers just weak at dealing with bits? > > Not a bug, but rather a missing feature: Jessie/Why3 does not send any > information about the bitwise-or operator to the provers, so the proof > obligations are not provable. > > That said, your other assumption was right nonetheless. Provers, while > not weak at dealing with bits (most of them natively support > bitvectors), tend to be weak when mixing bitvector and integer > arithmetics. By the way, they are also weak at nonlinear arithmetic, > hence your troubles when you tried non-constant rotations. > > Best regards, > > Guillaume > > _______________________________________________ > 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131108/de85d4f5/attachment.html>