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