--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on August 2015 ---
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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150817/6ed57aae/attachment-0001.html>