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] Arbitrary size fixed integer math

  • Subject: [Frama-c-discuss] Arbitrary size fixed integer math
  • From: kurt at roeckx.be (Kurt Roeckx)
  • Date: Sun, 25 Oct 2015 18:19:16 +0100
  • In-reply-to: <CAOH62Jh2_0T3vQO7u2VpjMA=9u54Gj1cLU4t7pYt=BKye5V=zA@mail.gmail.com>
  • References: <20151024120430.GA20528@roeckx.be> <CAOH62Jh2_0T3vQO7u2VpjMA=9u54Gj1cLU4t7pYt=BKye5V=zA@mail.gmail.com>
On Sun, Oct 25, 2015 at 06:05:09PM +0100, Pascal Cuoq wrote:
> Hello Kurt.
> 
> On Sat, Oct 24, 2015 at 2:04 PM, Kurt Roeckx <kurt at roeckx.be> wrote:
> 
> >
> > I was wondering if it would be possible to verify the math of the
> > BN library in OpenSSL. So I tried a little test program to see
> > what would happen.
> >
> 
> Your simplified program is definitely in scope for the deductive
> verification plug-ins WP and Jessie, and I say this with the serenity of
> one who does not have access to these tools today and is only going to
> provide vague hints and guesses throughout this message.

Thanks for all the hints, I'll know what to try next and let you
know what works and doesn't work.


Kurt