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

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