cil
cil copied to clipboard
Extern inline functions are handled incorrectly when `merge_inlines` is `false`
When merge_inlines
is false
, extern inline functions that are used several times produce one CFG with as many duplicate paths as there are usages. Here is an example to reproduce:
Details
// foo.h
extern __inline int ex()
{
return 0;
}
// bar.c
#include "foo.h"
void main() {
ex();
}
// baz.c
#include "foo.h"
void main() {
ex();
}
Goblint conf:
{
"files": ["bar.c", "baz.c"],
"cil": {
"merge": {
"inlines": false
}
}
}
Without the extern
, inline functions are handled fine: renaming the function with an added suffix and producing one separate CFG for each.