--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] math vs. bits



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