Conversion error when taking the address of a gcc built-in function

[andreast271]

CBMC fails to compile C code that takes the address of a GCC built-in function. Example:

int main() {
  void (*f)(int) = __builtin_exit;
  int (*g)(float) = __builtin_isnanf;
  (void) g(3.14f);
  f(1);
  return 0;
}

This code fails to compile and CBMC prints the following error message:

CBMC version 6.8.0 (cbmc-6.8.0-dirty) 64-bit x86_64 linux
Type-checking call
file call.c line 2 function main: failed to find symbol '__builtin_exit'
CONVERSION ERROR

[tautschnig]

We lack some built-in declaration and will fix this, but also I'm not entirely sure whether it is safe to take the address of those built-ins as some of them may compile to expressions rather than persisting as functions.