frama-clanguage-specificationsacsl

ACSL specification for a possibly infinite C function

I am trying to specify the behavior of external functions, more precisely, their termination. The ACSL documentation says that the \terminates p; property specifies that if the predicate p holds, then the function is guaranteed to terminate, but specifies nothing when p doesn't hold. It also explains that a function that never returns could be specified by:

//@ ensures \false ; terminates \false ;

Moreover ACSL provide a property \exits p; to specify the postcondition in case of abrupt termination. So I am wondering if:

//@ ensures \false ; exits \false; terminates \false ;

would specify that the function always loop forever ?

Moreover, what does the specification :

//@ ensures p ; exits q; terminates \false ;

means regarding to possible infinite loop ?

Solution

  • 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:

    1. Run-time error: you can always say that they are taken care of elsewhere (WP+genassigns or Value)
    2. longjmp: I'm afraid there is currently nothing in ACSL to specify something like that.