Transformation assert causes GNU inline merging problems with -O3

[J2000A]

During the implementation for my bachelor thesis about generating test cases for the incremental analysis I encountered a problem with the flag -O3. Possibly some merging problems with GNU inline? @stilscher

Reproduce by:
echo "main(){}" > input.c
./goblint input.c --enable trans.goblint-check --set trans.activated '["assert"]' --set pre.cppflags[+] -O3
./goblint transformed.c --set pre.cppflags[+] -O3 --enable incremental.save
./goblint transformed.c --set pre.cppflags[+] -O3 --enable incremental.load

This results in the error:
Fatal error: exception Failure("there can only be one definition and one declaration per global")

Output of cat transformed.c | grep pthread_equal:

__inline extern int ( __attribute__((__leaf__, __gnu_inline__)) pthread_equal)(pthread_t __thread1 ,
__inline extern int ( __attribute__((__leaf__, __gnu_inline__)) pthread_equal)(pthread_t __thread1 ,
__inline extern int ( __attribute__((__leaf__, __gnu_inline__)) pthread_equal)(pthread_t __thread1 ,
__inline extern int ( __attribute__((__leaf__, __gnu_inline__)) pthread_equal)(pthread_t __thread1 ,

vs when not using --set pre.cppflags[+] -O3:

extern int ( __attribute__((__leaf__)) pthread_equal)(pthread_t __thread1 ,

[michael-schwarz]

Is this only an issue for files that have been transformed using Goblint? If yes, I would once again suggest to move the issue over to the analyzer repository.

[J2000A]

Hey @michael-schwarz,
yeah you are right this also should go to the analyzer repo 👍

[J2000A]

I will repost this in the analyzer repo

[michael-schwarz]

I'll move it instead!

[sim642]

This could be the same CIL issue: goblint/cil#142. It's only in incremental comparison where Goblint carefully assumes and checks that the CIL invariant holds.