--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on August 2015 ---
At this point I come up against another oddity: ok = auth(buf,sz,& pay,& paysz); /*@ assert ok ⡠0 ⨠\initialized(pay+(0 .. paysz-1)); */ ; if (ok) { /*@ assert \initialized(pay+(0 .. paysz-1)); */ ; i = (unsigned int)0; while (i < paysz) { /*@ assert Value: initialisation: \initialized(pay+i); */ printf("%d\n",(int)*(pay + i)); i ++; } } here all the assertions are evaluated as valid except for the one before the printf. This is odd because the assertion above it says that pay[0..paysz-1] is valid and the value analysis knows that i is less than paysz at the printf. So why can't it discover that \initialized(pay+i) from \initialized(pay+(0..paysz-1)) ? On Mon, Aug 17, 2015 at 9:39 PM, Tim Newsham <tim.newsham at gmail.com> wrote: > ack, I apologize, I found it as "-val-split-return-auto" > and that did fix the analysis. Thank you! > > On Mon, Aug 17, 2015 at 9:22 PM, Tim Newsham <tim.newsham at gmail.com> > wrote: > >> Thank you. I tried this but it rejected the argument and I >> couldn't find any arguments with "split" in the name: >> >> $ frama-c --version >> Version: Sodium-20150201 >> Compilation date: Tue Aug 4 10:08:25 HST 2015 >> Share path: /usr/local/share/frama-c (may be overridden with FRAMAC_SHARE >> variable) >> Library path: /usr/local/lib/frama-c (may be overridden with FRAMAC_LIB >> variable) >> Plug-in paths: /usr/local/lib/frama-c/plugins (may be overridden with >> FRAMAC_PLUGIN variable) >> $ frama-c -kernel-help|grep split >> $ >> >> is the name bad or do I need to be on a different version? >> >> >> On Mon, Aug 17, 2015 at 8:57 PM, Anne Pacalet <anne.pacalet at free.fr> >> wrote: >> >>> Hi Tim, >>> >>> Le 18/08/2015 08:44, Tim Newsham a écrit : >>> > What is confusing me is that the assertion right after the call site >>> is the >>> > same (seems to me!) as the "ensures" clause of the implementation! So >>> why >>> > is the analyzer not drawing the connection? Is there something I can >>> do to >>> > help it out? >>> >>> I suspect that the states computed at the end of the function are merged >>> before >>> returning, so the assertion cannot be verified anymore on the merged >>> state. >>> Maybe you should try to use the option: >>> -val-split-return auto >>> or >>> -val-split-return-function auth:full >>> >>> Hope this helps. >>> >>> Anne. >>> _______________________________________________ >>> Frama-c-discuss mailing list >>> Frama-c-discuss at lists.gforge.inria.fr >>> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss >> >> >> >> >> -- >> Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | >> thenewsh.blogspot.com >> > > > > -- > Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | > thenewsh.blogspot.com > -- 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/20150817/52daa76f/attachment.html>