--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] math vs. bits



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>