Function contracts can be attached to function pointers as parameters

[nwetzler]

CBMC version: 5.63.0
Operating system: macOS 11.6.6
Exact command line resulting in the issue:
main.c

typedef void (*fun_ptr_t)(int x);

void bar(int x) {
  return;
}

void foo(void (*fun_ptr)(int x) __CPROVER_requires(x != 0)) {
  return;
}

void main() {
  fun_ptr_t fun_ptr = bar;
  foo(fun_ptr);
  return;
}

cbmc main.c

What behaviour did you expect:
Expected behavior is that a parsing error should occur.

What happened instead:
Function contracts are parsed and assigned to function pointer declarators in function parameters.

[martin-cs]

This is exciting; it is using the annotation almost as part of the type. I am not sure it is appropriate to do this at the parsing stage. For example if I have:

void baz (int x) __CPROVER_requires(x > 0) {
  return;
}

Can I foo(&baz) because x > 0 => x != 0? If so then we have to do an entailment check and that is really not viable as part of parsing.

More generally, thinking about Liskov's substitution principle, isn't what is required...

• precondition of function pointer => precondition of actual
• postcondition of actual => postcondition of function pointer
  I.E. the requires on the target of the pointer must be weaker than the function pointer annotation and the assumes of the target must be stronger than the function pointer annotation.

It's a non-trivial amount of work but it should be possible to add an instrumentation pass that checks these when assigning function pointers.

[jimgrundy]

Resolved by #7037