Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

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