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

Thanks Guillaume!

BTW I cannot get the function below to verify, even though it does not 
have the bitwise or.  Perhaps the division is causing problems?

Is there some way I can provide a bit of additional information here so 
these and the n-bit rotate functions verify, or am I stuck with an 
interactive proof assistant?

Of course I do not actually doubt the correctness of my rotate functions. 
Rather, I am trying to gauge how much use I can make of Frama-C in a 
course I'll be teaching in the spring.

John


/*@
   @ ensures (x % 2 == 0) ==> \result == x / 2 ;
   @ ensures (x % 2 != 0) ==> \result == x / 2 + INT32_MAX + 1 ;
   @ */
uint32_t rotate_right_1_a (uint32_t x)
{
   return (x >> 1) + (x << 31);
}




On Fri, 8 Nov 2013, Guillaume Melquiond wrote:

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