Add option include_stdlib to toggle inclusion of Goblint's stdlib.c

[michael-schwarz]

Always including Goblint's stdlib.c leads 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.

[sim642]

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.

[sim642]

Also I just grepped zstd's source and found no redefinition of qsort or bsearch, only calls to qsort included explicitly from stdlib.h. So I don't understand what the issue really was to begin with.

[michael-schwarz]

So I don't understand what the issue really was to begin with.

/usr/include/x86_64-linux-gnu/bits/stdlib-bsearch.h:19: Warning: def'n of func bsearch at /usr/include/x86_64-linux-gnu/bits/stdlib-bsearch.h:19 (sum 90592995) conflicts with the one at /home/michael/Documents/goblint-cil/analyzer/includes/stdlib.c:34 (sum 1086600); keeping the one at /home/michael/Documents/goblint-cil/analyzer/includes/stdlib.c:34.

[sim642]

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?

[michael-schwarz]

At closer look it's only bsearch though that's pulled in from "/usr/include/x86_64-linux-gnu/bits/stdlib-bsearch.h", so we would actually need to keep the Goblint qsort stub. I'm starting to wonder if we want to do this in a general way via cppflags?

E.g. we could have -DGOBLINT_NO_BSEARCH and would then check those in the headers.

[michael-schwarz]

Superseded by #584.