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



Dear David,

Thank you very much.


On 18 October 2013 08:40, David MENTRE <dmentre at linux-france.org> wrote:
>
>
> Well, because those functions are supposed to end the program (and
> thus are non terminating functions). :-) What would you have expected?
>

I am so sorry for not making it clear of my question.

I thought NON TERMINATING FUNCTION has no corresponding Pdg. But indeed,
the pdg was also constructed. so that would not be a problem now.

Thanks again.

Best regards,
-david
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131018/ed97a13f/attachment.html>