--- layout: fc_discuss_archives title: Message 79 from Frama-C-discuss on October 2013 ---
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>