--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on March 2009 ---
Le lundi 02 mars 2009 ? 17:39 +0100, David MENTRE a ?crit : > In above code, using Alt-Ergo 0.8, alt-ergo is unable to prove > property "assert rand_fd >= 0;". It seems obvious to me that the > exit() function never terminates. So, the only case that goes past the > "if (rand_fd < 0)" should be when "rand_fd >= 0", thus proving the > assert clause. This is apparently not the case. What have I missed? By the time function "main" is analyzed, the tools have forgotten the body of "exit"; they only have its (empty) specification. Try with the following specification, it should work: /*@ ensures \false; */ void exit(int err_code) ... Best regards, Guillaume