--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on November 2013 ---
On 08/11/2013 05:02, John Regehr wrote: > BTW I cannot get the function below to verify, even though it does not > have the bitwise or. Perhaps the division is causing problems? I took a look the proof obligations generated by Jessie and it is not the division that causes a problem (at least not yet). The issue is the way modulo arithmetic is encoded. While sufficient to prove your function, it is basically unusable. Indeed, modulo is defined in a subtractive way rather than by using the modulo operator. As a consequence, it is impossible to directly deduce anything about (x << 31) due to the combinatorial explosion (about four billion of billions of proof steps, if I did not get it wrong). The only sane way is to first prove that this subtractive modulo is in fact the traditional multiplicative modulo. So my guess is: it worked for a left rotation by 1, it should have worked for a rotation by 2, it might have failed for a rotation by 3, it will definitely fail for any larger rotation (e.g. 31 in your case). > 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? You are stuck with an interactive proof assistant, I guess. And even then it will be uglier than it should be. At this point, I think it is not reasonable to verify this kind of programs until a more adequate specification of modulo arithmetic is implemented in the tools. Best regards, Guillaume