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

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 ;
>  @ */