--- layout: fc_discuss_archives title: Message 10 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



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.