需要澄清 Aorai 的 frama-c YA 语言

Question

Aorai插件官方手册提供的例子https://frama-c.com/download/frama-c-aorai-manual.pdfexample.ya文件如下

%accept: S1, S2, S3, S4, S5, S6, S7;

S1 : { CALL(main)   } -> S2 
   ;
S2 : { opa().r>=0 } -> S3 
   ;
S3 : { opa().return<=5000 } -> S4
   ;
S4 : { !RETURN(opa) } -> S5
   ;
S5 : { RETURN(opb)  } -> S6
     ;
S6 : { RETURN(main) } -> S7
     ;
S7 :                  -> S7     
   ;

我的问题是为什么我们必须在状态 S4 指定 {!RETURN(opa)} 为什么我们不将其替换为 { CALL(opb) }？

这个自动机对应的主要函数是

int main() {
  if (rr<5000) rr=opa(rr);
  opb();
  goto L6;
  opc();
 L6:
  return 1;
}

Answer 1

!RETURN(opa) 表示当前事件必须 而不是 来自 opa 函数的 return。如果你看看整个自动机：

%init: S0;
%accept: S0, S1, S2,S3,S4,S5,S6;
S0 : { CALL(main) } -> S1;
;
S1 : { opa().r<5000 }
 -> S2
;
S2 : { opa().return<=5000 } -> S3
;
S3 : { !RETURN(opa) } -> S4
;
S4 : { RETURN(opb) } -> S5
;
S5 : { RETURN(main)} -> S6
;
S6 : -> S6
;

并考虑到每次调用或 return 事件都必须跨越转换，我们可以看到实际上这个事件必须是对 opb 的调用（这样我们就可以 return 从 opb 在从 S4 到 S5 的过渡期间。事实上，如果关于自动机的代码是正确的，则会调用 opa当处于状态 S1 时（参数小于 5000），后跟来自 opa 的 return（结果小于或等于 5000） , 将程序带回 main（从 S0 到 S1 的第一次转换是在程序开始时完成的）。

EDIT 更新原始问题后：从上面的描述中应该清楚，是的，S3 和 S4 之间的守卫可以写成 {CALL(opb)} 而无需真正更改规范。

需要澄清 Aorai 的 frama-c YA 语言

In need for clarification of Aorai's frama-c YA language

frama-c