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

Question

在使用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

Answer 1

不要忘记在每个事件中必须从自动机的当前状态进行转换。在这里，当您在 CALL 到 f 之后处于 S2 时，下一个发生的事件是 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;

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

What would be the automaton YA file corresponding to this C program?

frama-c