--- layout: fc_discuss_archives title: Message 23 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 01:01:02AM +0200, Kurt Roeckx wrote:
> On Sun, Oct 04, 2015 at 11:57:13PM +0200, Kurt Roeckx wrote:
> > On Wed, Sep 30, 2015 at 11:06:10PM +0200, Kurt Roeckx wrote:
> > > On Wed, Sep 30, 2015 at 12:11:26PM +0200, Boris Yakobowski wrote:
> > > > Hello again,
> > > 
> > > Thanks for taking the time to look at this.  I can see that your
> > > suggestion has some kind of effect, but it's not yet solving my
> > > problem.  I'll try to make a reduced case that still has my
> > > effect.  I've been adding more and more code but still don't see
> > > it.
> > 
> > So after spending some more time with it, I can prove most things
> > (in a somewhat reduced version), but I still seem to have a small
> > problem that I can't figure out.
> > 
> > I tried just substracting a small part of it, but then it has no
> > problem proving it.  I've attached my current test program.  Can
> > someone take a look at what I'm missing?
> 
> So looking at it some more, there seem to be 2 issues left.  When
> looking at it using Wp, at the end of HASH_UPDATE() there is:
>   if (len != (size_t)0) {
>     /*@ assert len <= \at(len,Pre); */ ;
>     /*@ assert data ? (data_+\at(len,Pre))-len; */ ;
>     /*@ assert \valid_read(data+(0 .. len-1)); */ ;

So it seems I got that part working, and Wp seems to be able to
prove everything.

Maybe it's me, but I find it very hard to find why it can't prove
something and I have to try random things until it's happy.

> 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.


Kurt