--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on November 2013 ---
Hello, 2013/11/8 John Regehr <regehr at cs.utah.edu>: > 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? I previously used a combination of Value analysis and WP to solve an issue with bitshift operations. The initial issue: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-August/003759.html Dillon Pariente solution: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-August/003764.html The general approach is to use Value to verify a limited set of cases with constant values (which is good at) and let WP generalize that to the generic case (which is good at). I don't know if such approach would work on your case, though. Best regards, david