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

[Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow



On Tue, Nov 4, 2014 at 9:01 AM, Virgile Prevosto
<virgile.prevosto at m4x.org> wrote:
> First of all, I'd say that for checking potential overflows in this
> context, Value Analysis could do the trick at least as easily as WP.
> The command line would be like this:


Thanks for your extensive follow up.

At some point in frustration I did try value analysis... but before
even being hit by the headers problem I found that it failed to report
overflows... it actually turns out that I was testing incorrectly: I
was setting the requires threshold greater than the input type size.
Doh.

With your help value analysis works great now, and on the whole function.