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



>
> Is the "ensures \false;" the standard way to specify non-terminating
> functions?

It is a standard way to specify that a program point is not reachable,  
yes.

> ACSL provides the "terminates" clause (ACSL ?2.5.4) but it
> is apparently unsupported by Jessie (Jessie doc ?7.2.3).

And it serves a different purpose anyway. "ensures \false;"
is a specification that can only be satisfied by a function that does
not terminate. "terminates \false;" is a specification that can
be satisfied by any function, since it only means that the function
does not have to terminate.

Pascal