goblint / cil

C Intermediate Language
https://goblint.github.io/cil/
Other
40 stars 16 forks source link

Rename functions with `gnu_inline` attribute when inline merging is off #85

Closed stilscher closed 2 years ago

stilscher commented 2 years ago

With gcc 4.3 the semantic of extern inline was changed to conform with the ISO C99 standard (https://gcc.gnu.org/gcc-4.3/porting_to.html). Functions that should still have the GNU extern inline behavior have the attribute __attribute__((__gnu_inline__)). A function with this attribute in a header that is included in multiple different translation units leads to multiple function variables with the same name. This violates the check that was added with https://github.com/goblint/analyzer/commit/39d72880888da8cc8aa65b914b90bbc174e7a3b7. By renaming function variables, that have this gnu_inline attribute, whenever inline functions are not merged, fixes this. Below is an example where the problem can be observed:

./goblint --enable incremental.save --disable incremental.load file1.c file2.c ./goblint --disable incremental.save --enable incremental.load file1.c file2.c or alternatively using --set pre.cppflags[+] -fgnu89-inline instead of the __attribute__((__gnu_inline__)) in the function definition

//file.h
extern inline __attribute__((__gnu_inline__)) int foo()
{ return 5; }
//file1.c
#include "file.h"
int goo() {
    return 2;
}
//file2.c
#include <assert.h>
#include "file.h"
int main() {
    int x = goo();
    assert(x == 2);
    return 0;
}