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