Your specification is the closest one that can amount to say that a function is looping forever, but I still see two corner cases left:
- Run-time error: you can always say that they are taken care of elsewhere (
WP
+genassigns
orValue
) - longjmp: I'm afraid there is currently nothing in ACSL to specify something like that.