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

[Frama-c-discuss] OpenSSL SHA256



On Mon, Oct 05, 2015 at 11:52:17PM +0200, Pascal Cuoq wrote:
> Hi Kurt,
> 
> On Mon, Oct 5, 2015 at 7:56 PM, Kurt Roeckx <kurt at roeckx.be> wrote:
> 
> >
> > > When I start it using Value again, I also get the
> > > uninitialized message again in sha256_block_data_order(),
> > > and can't seem to convince Value about it being initialized.
> >
> > Still have no idea about that one.
> >
> 
> Have you posted code, commandline used, tool version and generally
> everything necessary to reproduce yet?

I've attached a test program in one of my previous mails, it
should really show up with just frama-c -val. If you add an
-slevel to it, it might show a few more warnings, but that doesn't
even seem to be needed.

> I ask because as the initiator of an effort to get OpenSSL through Frama-C
> 's value analysis, I am in a particularly good position to point out that
> asking readers of this list to go through the effort of configuring OpenSSL
> for Frama-C in order to have a chance at a guess as to the problem you are
> encountering is asking too much.

I didn't know about any effort to get it through Frama-C, but
we've seen various other tools being used to find problems.

As stated before I was just really looking at it to see if it's
useful or not. I actually didn't discover any issue in the code I
was looking at. At least Wp seems to require a large effort before
it accepts things.

> My colleagues and I reported this bug, which you have already seen and
> which was fixed [1], and all those, which weren't [2]. So please consider
> working on getting these bugfixes through the system and into the code
> where they belong, instead of working at re-discovering the same ones.

We still have problems keeping up with all the reported issues.
But I'll try to look at them soon.


Kurt