cil
cil copied to clipboard
Handling of static functions with a name ending in `__extinline`
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