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

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>