goblint / cil

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

Preserve `fundec` location in merger #139

Closed sim642 closed 1 year ago

sim642 commented 1 year ago

Function definitions GFun share the varinfo with all of its declarations (GVar/GVarDecl). Within a single file, Cabs2cil prefers the definition's location for the function variable: https://github.com/goblint/cil/blob/986a509d85417a55b4c98e635e3d52abb7e85b3f/src/frontc/cabs2cil.ml#L1939-L1942

Turns out that Mergecil doesn't and simply keeps the first one. So depending on the order of merged files, it may be given a declaration's location from a header, even though a definition exists in another file. For consistency definition locations should also be preferred during merging.