--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on November 2013 ---
By the way, the topic of rotate comes up because I have lately been looking at open source crypto libraries and have found numerous bugs related to rotate. Not bugs in the rotate functions, but rather undefined behaviors where the rotate functions' preconditions are violated. Pascal, I do not know if your adventures in specification and verification have taken you into crypto-land, but if they have, we should talk! Anyhow, I have one more question: I'd like to specify an n-bit rotate as repeated application of the specification for 1-bit rotate, such as we see below. I could not think of an elegant way to do this in ACSL. Is it possible? Thanks, John Regehr > /*@ > @ ensures (x % 2 == 0) ==> \result == x / 2 ; > @ ensures (x % 2 != 0) ==> \result == x / 2 + INT32_MAX + 1 ; > @ */