--- layout: fc_discuss_archives title: Message 79 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [value analysis] calls the system library function abort or exit will result in NON TERMINATING FUNCTION. Why?



uhm, Thank you very much.


On 21 October 2013 19:43, Boris Yakobowski <boris at yakobowski.org> wrote:

> Hi,
>
> NON TERMINATING FUNCTION means that the final statement of the
> function is either unreachable, or results in an error ; this also
> implies that the control does not return to the caller. This is indeed
> the case for functions that call exit (), and is automatically handled
> by the various plugins derived from Value. To determine if a function
> returns, Frama-C/Cil either read GCC's
> __attribute__ ((noreturn)) (that is present in system headers), or
> uses 'ensures \false' clauses, as suggested by David.
>
> On Fri, Oct 18, 2013 at 1:29 PM, David Yang <abiao.yang at gmail.com> wrote:
> > I thought NON TERMINATING FUNCTION has no corresponding Pdg. But indeed,
> the
> > pdg was also constructed. so that would not be a problem now.
>
>
>
> --
> Boris
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131021/7f289836/attachment.html>