readthedocs CI failing is unrelated.

readthedocs CI failing is unrelated.

I added a workaround on master.

The big issue with not merging inlines is still there, silently breaking our assumptions: goblint/cil#84 and 62d7591#commitcomment-67629901. So I don't understand why you really want to avoid merge_inlines instead of fixing the merging errors we get with it enabled instead.

So I don't understand why you really want to avoid merge_inlines instead of fixing the merging errors we get with it enabled instead.

I don't think it is doing one to the exclusion of the other. This fix allows us to go ahead with our benchmarks without any issues. We should at some future point also fix the merging of inlines (even though I personally find the notion of doing that a bit dubious), but CIL should still work when it is disabled.

Note that it would be perfectly sensible for code to provide two different extern inline functions of the same name in two different compilation units when declaring the gnu_inline function attribute, so this code is needed regardless.

I don't think I understand in what sense any invariant is broken here? The one-to-one correspondence between a fundec and its varinfo is still there (as before), the only difference now is that the names of the corresponding varinfos are also globally unique.

And if it is indeed problematic what does it have to do with inline? Is it not equally problematic for static functions then?

This fix allows us to go ahead with our benchmarks without any issues.

goblint/cil#84 breaks the internal invariant silently. Unless we manually trace and check all the varinfo and fundec objects having one-to-one mapping, the problem with accidental physical object sharing is so subtle that CIL nor Goblint print any warnings about it (and I'm not sure how they even could).
That undesired sharing was the sole reason for massive CFG construction time and memory usage: #603 (comment). Just this single issue caused by goblint/cil#84 took us weeks to hunt down.
So there's no telling that Cfg.prev during the analysis itself doesn't cause each copy of each (unmerged) inline function to be analyzed a quadratic number of times, instead of linear, because all the copies have all other copies as their bodies as well.

We should at some future point also fix the merging of inlines (even though I personally find the notion of doing that a bit dubious), but CIL should still work when it is disabled.

What is the problem with merging inlines though, other than inefficiency? I don't at least see any open issue about it which could be a threat to validity by breaking AST invariants.

Note that it would be perfectly sensible for code to provide two different extern inline functions of the same name in two different compilation units when declaring the gnu_inline function attribute, so this code is needed regardless.

And that's exactly why I'm concerned here: goblint/cil#85 (comment). There are inconsistencies on top of goblint/cil#84:

1. Two different extern inline functions with the same name shouldn't be merged regardless of the __gnu_inline__ attribute, so it's weird that the renaming depends on that.
2. When __gnu_inline__ changes the semantics of inline functions, then that should also affect the merging of their bodies, not just their renaming.

I don't think I understand in what sense any invariant is broken here? The one-to-one correspondence between a fundec and its varinfo is still there (as before), the only difference now is that the names of the corresponding varinfos are also globally unique.

Actually this might even be accidentally fixing the broken invariant, but just for the __gnu_inline__ functions because instead of having the undesired varinfo sharing, it forces a rename.

And if it is indeed problematic what does it have to do with inline? Is it not equally problematic for static functions then?

Given that the function merging code is spread into two different places to control the varinfo renaming and the body merging, that might also be the case. I don't think we do any real testing with static functions either.

Waiting for goblint/cil#86 to land, and update then