Aorai 的 LTL 配方

Question

我正在尝试查找有关 LTL 运算符 _ F_ 的示例，这对 Aorai 来说是致命的，但我无法弄清楚该运算符的确切目标，并且 Aorai 的存储库 "tests" 中没有示例比如我写了这个公式

CALL(main) && _X_ (CALL(a) && _X_(RETURN(a) && _F_ (RETURN(b) && _X_ (RETURN(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 和 return 紧随其后。

注意：请注意，Aorai 仅跟踪调用和 return 事件，因此例如这里的"just after"是指main在最后一次调用b之后不能再调用任何函数，但是仍然可以执行一些动作，比如x++;.

更新我有运行你在 Frama-C 上的完整示例。事实上，Aorai 为 main 生成的合约中缺少一个 post 条件，即假设在 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）

Aorai 的 LTL 配方

LTL Formula with Aorai

frama-c