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