Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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