Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] arbitrary buffers in analysis
- Subject: [Frama-c-discuss] arbitrary buffers in analysis
- From: tim.newsham at gmail.com (Tim Newsham)
- Date: Thu, 27 Aug 2015 18:40:02 -0700
- In-reply-to: <CABbVA-BSAJkUYZD1+kC0xn8H_yXON=Ld-cyPnPa3WnLrWS3V6g@mail.gmail.com>
- References: <CAGSRWbgQaaaBnjhBWamzidNa4Q+rqwoeJY9NDir98jebQFzmfQ@mail.gmail.com> <55D587D9.2080300@linux-france.org> <CAGSRWbg_bsifsWpGGb8Z0-40ZZbhW5aAOw-5L4Np+r0vrA2jbA@mail.gmail.com> <CAOH62Jg58aD+5Z4Hgv4ZtNff9giXZagoQgLj=L-TT3shQztfWw@mail.gmail.com> <CABbVA-BSAJkUYZD1+kC0xn8H_yXON=Ld-cyPnPa3WnLrWS3V6g@mail.gmail.com>
On Wed, Aug 26, 2015 at 3:01 PM, Boris Yakobowski <boris at yakobowski.org> wrote: > Interestingly, most of those useless tests can be waived by rewriting the > main function in the following way: > > //@ assigns p[0..size-1] \from \nothing; ensures > \initialized(&p[0..size-1]); > void init_buf(char *p, unsigned int size); > > > int run(unsigned int sz, unsigned int ksz) > { > [..] > /* init buf[0..sz-1] and kbuf[0..ksz-1] */ > init_buf(buf, sz); > init_buf(kbuf, ksz); > [..] > } > > void main() { > for (unsigned int sz=0; sz<MAXBUFSZ; sz++) > for (unsigned int ksz=0; ksz<MAXKEYSZ; ksz++) > run(sz, ksz); > } > > Using this driver -- plus option -memexec-all, which speeds things up > significantly -- the analysis takes 55 minutes and > Thank you.. this is exactly the type of feedback I was hoping for. One question: what is -memexec-all? I see it mentioned briefly in the value help, but not in the frama-c manual. > proves everything except the assertion > /*@ assert \initialized(buf + (32..40)); */ > > This is good because > - I'm not convinced it is a true assertion > - /*@ assert \initialized(buf + (32..39)); */ is sufficient, and can be > proven > hrmm.. indeed.. this scares me because my previous analysis didnt catch this! > Boris > Also thank you for the other email about the fopen issue. I don't recall fopen reporting dead code in my model of fopen but I'll revisit the issue as I digest the ideas in your email further. -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150827/a11d8d4a/attachment.html>
- Follow-Ups:
- [Frama-c-discuss] arbitrary buffers in analysis
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] arbitrary buffers in analysis
- From: boris at yakobowski.org (Boris Yakobowski)
- [Frama-c-discuss] arbitrary buffers in analysis
- References:
- [Frama-c-discuss] arbitrary buffers in analysis
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] arbitrary buffers in analysis
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] arbitrary buffers in analysis
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] arbitrary buffers in analysis
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] arbitrary buffers in analysis
- From: boris at yakobowski.org (Boris Yakobowski)
- [Frama-c-discuss] arbitrary buffers in analysis
- Prev by Date: [Frama-c-discuss] Speedup Frama-C/WP generating proof obligations
- Next by Date: [Frama-c-discuss] arbitrary buffers in analysis
- Previous by thread: [Frama-c-discuss] arbitrary buffers in analysis
- Next by thread: [Frama-c-discuss] arbitrary buffers in analysis
- Index(es):