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

  • Subject: [Frama-c-discuss] OpenSSL SHA256
  • From: kurt at roeckx.be (Kurt Roeckx)
  • Date: Tue, 6 Oct 2015 09:11:42 +0200
  • In-reply-to: <CAOH62JhQczyRsSzCcPmfaN5yEc+VBbd2CAgWSHRGVaXt3==LtQ@mail.gmail.com>
  • References: <20150928213423.GA19993@roeckx.be> <CABbVA-DEJCXcJnwUwNM6YpG22-9UVknvsYyx=40FsEhgcc35Cg@mail.gmail.com> <20150930210610.GA4289@roeckx.be> <20151004215712.GA27389@roeckx.be> <20151004230102.GA765@roeckx.be> <20151005175630.GA18032@roeckx.be> <CAOH62JhQczyRsSzCcPmfaN5yEc+VBbd2CAgWSHRGVaXt3==LtQ@mail.gmail.com>
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