goblint / cil

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

Fix merging and renaming of inlines #124

Closed stilscher closed 1 year ago

stilscher commented 1 year ago

The renaming of inline functions was broken in that multiple functions with the same name were outputted in the merged CIL file. This also lead to difficulties with the incremental analysis in Goblint, because globals are expected to have a unique name (https://github.com/goblint/analyzer/pull/836). Also, the merging of inline functions was not correct, because inline functions with different bodies would not be renamed and the wrong version of a function would be called.

This PR aims at fixing that. For this, a distinction is made which C Standard is used, i.e. whether the gnu89 or c99 inline semantics needs to be used. They differ in that for c99 inline functions have internal linkage by default, unless extern inline is used, whereas it is opposite for gnu89. They agree on static inline functions that can in both cases only be called from the same translation unit.

This is reflected in the following changes:

Closes #120

sim642 commented 1 year ago
  • All internal inline functions are renamed to avoid duplicate names. When inline functions are successfully merged, this renaming is reverted.

That means if only a single file containing inline functions is involved, so no merging happens at all, then it won't have its original name even though it's the easiest case where it should have?

stilscher commented 1 year ago

That means if only a single file containing inline functions is involved, so no merging happens at all, then it won't have its original name even though it's the easiest case where it should have?

No, that is not the case. Renaming here means, it finds a new name (e.g. add__0) only if another function with the same name was already encountered. Otherwise the original name (e.g. add) is just kept.

michael-schwarz commented 1 year ago

LGTM!