Diverging functions do not need to modify state

[shym]

Currently gospel check rejects:

val run : unit -> unit
(*@ run ()
    diverges *)

with:

Error: The function `run' returns `unit'
       but its specifications does not contain any `modifies' clause.

We could consider that:

• the function that only diverges should be ruled out,
• or modifies (), or something similar, is the canonical annotation for such cases,
• or that diverges or modifies would be required for unit-returning functions.

[n-osborne]

gospel check should indeed at least accept this specification for the run function.
An other example is the sleep function, that does not diverge but returns unit without modifying anything (that we can express in the specification).

I'm thinking that having the absence of modifies clause for unit-returning function as an error may be a bit too strong. A warning may be more appropriate.