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

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