--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on October 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Arbitrary size fixed integer math



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