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



Hello David,

2013/10/17 David Yang <abiao.yang at gmail.com>:
> While analyzing a function which calls the system library function (abort or
> exit), the value analysis result is non terminating function.
>
> Why?

Well, because those functions are supposed to end the program (and
thus are non terminating functions). :-) What would you have expected?

> 1. command for the value analysis of the tesing function in test.c file:
>
> $: frama-c -lib-entry -main test_abort test.c -val
> $: frama-c -lib-entry -main test_abort test.c -val

But your real question might be: how Frama-C determines that such
functions are not terminating?

I thought that the following annotation (ensures \false;) would be
used, but as you don't seem to use standard Frama-C header, maybe this
is built-in in Frama-C or Value, I don't know.

In share/frama-c/libc/stdlib.h:
"""
/*@
  assigns \nothing;
  ensures \false;
*/
void exit(int status);
"""

Best regards,
david