stilscher
commented
2 years ago What do you mean with physical object? The invariant just says, that all references to a function must point to the same varinfo. So different instances of a function (for example two instances of a static inline function that has not been merged) could still have different varinfos as long as they are consistent with the respective function calls, right?
fundecclaims the invariant that the physical objects are in one-to-one correspondence withvarinfos: https://github.com/goblint/cil/blob/c47bbbdb442b4d50dac5a0879404ab3b5592170a/src/cil.ml#L688-L694 And Goblint relies on this invariant by identifying functions by the underlying variable (ID).In https://github.com/goblint/analyzer/pull/603#issuecomment-1054204635, I realized that https://github.com/goblint/cil/pull/72 broke this invariant. This is also easily seen in the code: https://github.com/goblint/cil/blob/c47bbbdb442b4d50dac5a0879404ab3b5592170a/src/mergecil.ml#L1421-L1425 where the underlying variable is replaced unconditionally (of
merge_inlines).