这个 C 程序对应的自动机 YA 文件是什么？

问题描述

在使用 frama-c 的 Aorai 插件验证这个程序的上下文中，.ya 文件格式的相应自动机是什么？

void f() {
    ;
}

void g(){
    ;
}

int main(){
    f();
    g();
    return 0;
}

我的猜测是这个

%init: S0;
%accept: S4;

S0 : { CALL(main) } -> S1
   ;
S1 : { CALL(f) } -> S2
   ;
S2 : { CALL(g) } -> S3
   ;
S3 : {RETURN(main) } -> S4
   ;
S4 : -> S4
   ;

但我使用 Aorai 插件时出现此错误

[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[aorai] Threestateaut.c:12: Warning: 
  Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path

解决方法

不要忘记在每个事件中必须从自动机的当前状态进行转换。在这里，当您在 S2 到 CALL 之后的 f 中时，发生的下一个事件是从 RETURN 到 f 的 main，但从 S2 的唯一转换由 CALL(g) 保护（因此自动机的开头描述了一个程序，其中 f 本身调用 g）。

要解决此问题，您可以将 RETURN 考虑在内，如

...
S2: { RETURN(f) } -> S3;
S3: { CALL(g)   } -> S4;
...

或使用 YA 扩展（如 section 3.1.3 of the manual 中所述，它特别允许指示您有一个 CALL(f) 直接后跟一个 RETURN(f) ：

...
S2: { f() } -> S3;
...

实际上，通过这些扩展，可以以更紧凑的方式指定完整的执行流程，因为您可以嵌套调用序列：

%init: S0;
%accept: S1;

S0 : { main([f();g()]) } -> S1;

S1: -> S1;