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] WP failing to prove a simple absence of RTE unsigned overflow

  • Subject: [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
  • From: gmaxwell at gmail.com (Gregory Maxwell)
  • Date: Tue, 4 Nov 2014 09:24:21 +0000
  • In-reply-to: <CA+yPOVi8gW53yUTm6dYXLV_TeVa_=czKB02k-ZqJZLnPsd180Q@mail.gmail.com>
  • References: <CAAS2fgRTEAODJ78tg7m77oDEyK4XG0E0GHLRkrqm7tRNFwY3bg@mail.gmail.com> <CA+yPOVi8gW53yUTm6dYXLV_TeVa_=czKB02k-ZqJZLnPsd180Q@mail.gmail.com>
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.