--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on August 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] arbitrary buffers in analysis



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>