Function call in a "if" clause to ACSL

Question

Consider the following code

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

The response of frama-c to the following code is the following error

[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.

Is there a way to write a specification where there's a call of a function inside an "if" clause ?

user_4628125 · Answer

In ACSL, you cannot use a C function in the specification. If you want to do something like this, the only possibility is to define a logic function (ideally provably) equivalent to the C function and to use this logic function.

/*@ 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;
}

Function call in a "if" clause to ACSL

1 Answers