3

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 ?

Daniel Trebbien
  • 38,421
  • 18
  • 121
  • 193
Anne
  • 1,270
  • 6
  • 15

1 Answers1

1

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.
Virgile
  • 9,724
  • 18
  • 42
  • Thank you for your answer. About run time error, I thought of that but you cannot expect specifying RTE, can you ? About longjump, I think that I can ignore them for the moment. Thanks again. – Anne Feb 25 '13 at 13:40