Handling of static functions with a name ending in `__extinline`

[michael-schwarz]

Static functions with a name ending in __extinline are handled incorrectly, when a prototype is provided for them.

static int bla__extinline();

static int bla__extinline() {
    return 0;
}

int main(void) {
    bla__extinline();
    return 0;
}

is transformed into

#line 1 "1.c"
static int bla__extinline() ;
#line 3
__asm__("error in function bla__extinline");
#line 7 "1.c"
int main(void) 
{ 
  {
#line 8
  bla__extinline();
#line 9
  return (0);
}
}

by CIL where the function definition is missing, while emitting a warning

Error: It seems that we would need to rename global bla__extinline (to bla__extinline___0) 
  because of previous occurrence at 1.c:1
  Context : 2cil: bla__extinline
error in collectFunction bla__extinline: Errormsg.Error

If there is no prototype for the function, or it is not static, the issue does not happen.

Cil internally renames external inline functions to have the suffix __extinline, so it becomes confused there.

In Goblint, this poses a soundness issue depending on what we assume unknown functions may do. (sem.unknown_function.invalidate.globals, sem.unknown_function.spawn)

Old relevant messages on the CIL mailing list: https://cil-users.narkive.com/LAMqUU85/cil-users-extinline-problem