--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on November 2013 ---
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); }