search

goblint / cil

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

Cil keeps inline and non-inline function with same name #120

Closed jerhard closed 1 year ago

jerhard commented 2 years ago

As noted by @stilscher in https://github.com/goblint/analyzer/issues/836#issuecomment-1289167201, the merging in Cil does not behave correctly for inline functions.

I created a small example to test the open questions that @jerhard posted above. It seems that the merger is not behaving correctly. If merge_inline is disabled a function definition and an inline function definition with the same name but in a different translation unit do not get merged but are not renamed either. This is also the case when merge_inline is enabled but the function bodies are not the same. I will take a look at the merger and try to fix it, in a way that multiple function definitions either get a unique name or are merged.

michael-schwarz commented 2 years ago

I think this might be in compliance to the pre-C99 GNU inlining semantics, we need to carefully think this through.

jerhard commented 2 years ago

Indeed, gnu89 allows for this. Also the meaning of extern inline and inline are swapped (except that extern inline in gnu89 allows redefinition, while c99 inline does not) in gnu89 and c99. One might have to handle this depending on the set language standard. I am not sure whether this is already handled in some way?

michael-schwarz commented 2 years ago

There's an option enable or disable C99 mode, but I don't think it is consulted here. When I extended inline support I focussed on adding some cases that C99 allows, that GNU90 C did not, but it was en example-program driven effort, I never stopped to carefully consider all cases.