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

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.

有没有办法编写规范，其中在“if”子句中调用函数？

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;
}