--- layout: fc_discuss_archives title: Message 55 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



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
>