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] OpenSSL SHA256



On Tue, Oct 06, 2015 at 07:06:23PM +0200, Pascal Cuoq wrote:
> On Tue, Oct 6, 2015 at 9:11 AM, Kurt Roeckx <kurt at roeckx.be> wrote:
> 
> >
> > I didn't know about any effort to get [OpenSSL] through Frama-C
> >
> 
> Analyzing OpenSSL is not the goal of the project per se, but the CII-funded
> "False-Positive-Free Testing" project aims at adding to the palette of
> tools offered by Frama-C one that is easier to use. "Easier" meaning:

I knew that CII was funding something Frama-C related, but not
exactly what, I guess I didn't read it properly, forgot parts of
it, ...  But that was why I started looking at Frama-C.

> Right now a few changes are still necessary in OpenSSL's source code to
> apply the tool being developed to it, though. Some are to work around
> limitations in the tool. The limitations are being worked on. And other
> changes are to fix existing bugs, so this is why it would be valuable if
> the fixes were integrated in the development version. (I know they are for
> minor defects. Fixing them makes it more pleasant to apply a tool that will
> find major defects too as they might be introduced.)

I'm going thru them now.  Rich actually replied to your mail, but
it wasn't clear what his concerns really are and then probably
forgot about them.  At least a few should be easy to get applied.


Kurt