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

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

Function call in a "if" clause to ACSL

static-analysis

frama-c