对 ACSL 的 "if" 子句中的函数调用

Question

考虑以下代码

int f(int a, int b){
return 0;
}
/*@
ensures (f(2,3)== 0) ==> result == 2;
*/
int g() {
if (f(2,3) == 0)
return 2;
return 0;
}

frama-c对以下代码的响应是以下错误

[kernel:annot-error] fing.c:5: Warning: 
unbound function f. Ignoring logic specification of function g
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "fing.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.

有没有一种方法可以编写一个规范，其中在"；如果"；条款

Answer 1

在ACSL中，不能在规范中使用C函数。如果你想做这样的事情，唯一的可能性是定义一个等价于C函数的逻辑函数(理想情况下是可证明的(，并使用这个逻辑函数。

/*@ logic integer l_f(integer a, integer b) = 0 ; */
//@ ensures result == l_f(a, b);
int f(int a, int b){
return 0;
}
/*@
ensures (l_f(2,3)== 0) ==> result == 2;
*/
int g() {
if (f(2,3) == 0)
return 2;
return 0;
}