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

  • Subject: [Frama-c-discuss] math vs. bits
  • From: regehr at cs.utah.edu (John Regehr)
  • Date: Thu, 07 Nov 2013 20:25:27 -0700
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);
}