Add option include_stdlib to toggle inclusion of Goblint's stdlib.c
#576
Conversation
There was a problem hiding this comment.
I think this should be more general than specific to stdlib.c and bsearch/qsort.
As a possible workaround for goblint/bench#15, where the pthread.c stub including pthread.h causes merge conflicts with the 32-bit versions of types that have been hard-included into the combined benchmarks, I tried to avoid the include:
6ea4b3f
But I had to immediately revert it because MacOS CI failed since the typedef is apparently different there.
So in that light, we should allow excluding any of our stubs. The best way to do that would be to have an option like stubs with the default value ["stdlib.c", "pthread.c"]. Then the default behavior would try to be sound, but for crazy programs it's possible to exclude specific stubs.
|
Also I just grepped zstd's source and found no redefinition of |
|
|
Neither of those come from zstd though. The conflict is with an extern inline function from your version of the standard library headers. I think we have some CIL issue related to those extern inlines because CIL tries to do something special with them. Maybe disabling compiler optimizations gets rid of the extern inline version? |
|
At closer look it's only E.g. we could have |
|
Superseded by #584. |
Always including Goblint's
stdlib.cleads to merge conflicts for any projects that do define those functions themselves (e.g. in goblint/bench#16).Add an option to disable this inclusion which produces much cleaner CIL merges for such projects.