Extern inline functions are handled incorrectly when `merge_inlines` is `false`

[karoliineh]

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.

[sim642]

#85, #86 and #123 are all related to this but somehow still didn't fix everything.

The problem might be related to the inconsistency I pointed out here: https://github.com/goblint/cil/pull/85#discussion_r834448283. Slightly different logic is used to determine whether their varinfos are merged and whether the function bodies are merged. In this case the varinfos are merged (not renamed), but function bodies are not. The result is that file.globals ends up containing one GFun for each copy with a physically different body, but they all physically share the varinfo.

[michael-schwarz]

Is this also a problem with valid programs? The one given above (after fixing that there is two main functions), yields the following output when compiled and linked with gcc:

michael@michael-ThinkPad-X1-Carbon-6th:~/Documents/goblint-cil/analyzer/tests/others$ gcc bar.c baz.c
/tmp/ccSG2c32.o: In function `ex':
baz.c:(.text+0x0): multiple definition of `ex'
/tmp/ccQ2HpGq.o:bar.c:(.text+0x0): first defined here
collect2: error: ld returned 1 exit status

Otherwise I am not sure what the meaning of "correct" even is here...

[sim642]

The unminimized issue is from silver searcher and some extern inline functions from the stdio.h header, which are certainly valid.

From bits/stdio2.h:

__fortify_function int
__NTH (vasprintf (char **__restrict __ptr, const char *__restrict __fmt,
		  __gnuc_va_list __ap))
{
  return __vasprintf_chk (__ptr, __USE_FORTIFY_LEVEL - 1, __fmt, __ap);
}

which preprocesses to

extern __inline __attribute__ ((__always_inline__)) __attribute__ ((__artificial__)) int
__attribute__ ((__nothrow__ , __leaf__)) vasprintf (char **__restrict __ptr, const char *__restrict __fmt, __gnuc_va_list __ap)

{
  return __vasprintf_chk (__ptr, 2 - 1, __fmt, __ap);
}