--- layout: fc_discuss_archives title: Message 13 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 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)); */ ;

and it can't prove that \valid_read for some reason.

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.  I
would of course like to see both go away if possible.


Kurt