LTL Formula with Aorai

Question

I am trying to find an example about the LTL operator _ F_ which means fatally with Aorai but i can't figure out exactly what this operator aims and there are no examples in the repository "tests" of Aorai For example, i wrote this formula

CALL(main) && _X_ (CALL(a) && _X_(RETURN(a) && _F_ (RETURN(b) && _X_ (RETURN(main)) ) ))

which says that in my program main, i have to call the function a() and after this i don't understand what happens with the operator fatally but it seems that it takes and accepts whatever we call after the function a() with no warning or error from Aorai. If anybody could help me or could give a right example about it. For example, i have this program below which i would like to test with this formula above

void a() 
{}
void b() 
{}
int main() 
{ a();
  a();
  b();
  b();
  a();
  return 0;}

I type frama-c -aorai-ltl test.ltl test.c Normally, there should be an error or warning from Aorai. No?

Answer 1

Your question is more about temporal logic than Frama-C/Aorai itself, but the meaning of this formula is that main must call a, then do whatever it wants, before calling b and returning just after that.

NB: note that Aorai only traces call and return events, so that e.g. "just after" here means that main cannot not call any function after its last call to b, but can still perform some actions, such as x++;.

Update I've run your complete example on Frama-C. Indeed a post-condition is missing in the contract for main generated by Aorai, namely that the state of the generated automaton at the end of main (T0_S4) is supposed to be accepting, which is not the case here. This is a bug. If you write explicitely an equivalent automaton in the ya language, as

%init: S0;
%accept: Sf;

S0: { CALL(main) } -> S1;

S1: { [ a() ] } -> S2;

S2: { RETURN(b) } -> S3
  | other -> S2;

S3: { RETURN(main) } -> Sf;

Sf: -> Sf;

Then the generated contract for main contains a requires \false;, which indeed indicates that the function is not conforming to the automaton, and Aoraï warns about that.

Please note however that in the general case, Aoraï will not emit any warning. It generates contracts that, if fulfilled, imply that the whole program is conforming to the automaton. The proof of the contract must be done by another plugin (e.g. WP or Value Analysis)