Формула LTL с Aorai

Question

Я пытаюсь найти пример об операторе LTL _ F_, что фатально означает для Aorai, но я не могу точно выяснить, для чего предназначен этот оператор, и нет примеров в "тестах" хранилища Aorai. Например, я написал эту формулу

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

который говорит, что в моей программе main, я должен вызвать функцию a(), и после этого я не понимаю, что происходит с оператором фатально, но кажется, что он принимает и принимает то, что мы вызываем после функции a() без предупреждение или ошибка от Aorai. Если кто-нибудь может мне помочь или может дать правильный пример по этому поводу. Например, у меня есть эта программа ниже, которую я хотел бы проверить с этой формулой выше

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

Я печатаю frama-c -aorai-ltl test.ltl test.cОбычно должно быть сообщение об ошибке или предупреждение от Aorai. Нет?

Answer 1

Ваш вопрос больше касается временной логики, чем самого Frama-C/Aorai, но смысл этой формулы в том, что main должен позвонить aпотом делай что хочешь, прежде чем звонить b и возвращаясь сразу после этого.

NB: обратите внимание, что Aorai отслеживает только события вызова и возврата, так что, например, "сразу после" здесь означает, что main не может вызвать любую функцию после ее последнего вызова b, но все еще может выполнять некоторые действия, такие как x++;,

Обновление Я запустил ваш полный пример на Frama-C. Действительно, в контракте отсутствует постусловие main сгенерированный Aorai, а именно, что состояние сгенерированного автомата в конце main (T0_S4) должен принимать, что здесь не так. Это ошибка. Если вы напишите явно эквивалентный автомат в ya язык, как

%init: S0;
%accept: Sf;

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

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

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

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

Sf: -> Sf;

Затем сгенерированный контракт на main содержит requires \false;Это действительно указывает на то, что функция не соответствует автомату, и Aoraï предупреждает об этом.

Обратите внимание, однако, что в общем случае Aoraï не будет выдавать никаких предупреждений. Он генерирует контракты, которые, если они выполнены, подразумевают, что вся программа соответствует автомату. Подтверждение контракта должно быть сделано другим плагином (например, WP или Value Analysis)