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”子句中调用函数？

标签： static-analysisframa-c

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