--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on March 2009 ---
> > 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