--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Issue with non terminating function



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