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