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



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?

My goal today was to verify some rotate-by-n functions but that turned 
out to be unexpectedly ambitious so I'm trying rotate-by-1 first.

John



/*@
   @ ensures x <= INT32_MAX ==> \result == 2 * x ;
   @ ensures x > INT32_MAX ==> \result == 2 * x - UINT32_MAX;
   @ */
uint32_t rotate_left_1_a (uint32_t x)
{
   return (x << 1) + (x >> 31);
}

/*@
   @ ensures x <= INT32_MAX ==> \result == 2 * x ;
   @ ensures x > INT32_MAX ==> \result == 2 * x - UINT32_MAX;
   @ */
uint32_t rotate_left_1_b (uint32_t x)
{
   return (x << 1) | (x >> 31);
}