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