--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on March 2009 ---
Hello Guillaume, On Mon, Mar 2, 2009 at 19:03, Guillaume Melquiond <guillaume.melquiond at inria.fr> wrote: > By the time function "main" is analyzed, the tools have forgotten the > body of "exit"; they only have its (empty) specification. Ok, I overlooked that. > Try with the > following specification, it should work: > > /*@ ensures \false; */ > void exit(int err_code) ... It worked. Thanks! Is the "ensures \false;" the standard way to specify non-terminating functions? ACSL provides the "terminates" clause (ACSL ?2.5.4) but it is apparently unsupported by Jessie (Jessie doc ?7.2.3). Yours, d.