--- layout: fc_discuss_archives title: Message 14 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



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>