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