--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on October 2015 ---
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