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

[Frama-c-discuss] trouble debugging assertions



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>