Function forward-declarations mishandled in incremental compare and update

[sim642]

See https://github.com/goblint/analyzer/pull/609#issuecomment-1057333884 and the following comments.

Special care should be taken of GVarDecls that also have corresponding GFuns. The CIL invariant is that if they refer to the same function, they should share a single physical instance of varinfo. Currently incremental compare and update treats them separately and may update the ID twice, while also breaking the sharing. I suppose we'll have to group all the GVarDecls for a GFun together and do a single update to the varinfo, which is shared by all of them.

[sim642]

@stilscher Actually the problem described here wasn't about comparing function declarations, although I guess with the uniqueness check it might already fail during comparison. The issue was with updating the IDs, which is done by iterating over all the globals to number them sequentially, while the declarations and definitions (correctly) share a varinfo. I think here it's not possible to completely ignore them (and they're not updated when updating functions that reference them) because even unused declarations should get fresh IDs that don't accidentally collide with anything else. Hence the fix to UpdateCil might have to be a bit more involved. For example, first grouping all the to-be-updated globals by their varinfos (which would put a definition together with all the connected declarations) and just update that once.

[michael-schwarz]

@stilscher Is this still the case or is it fixed now?

[stilscher]

It is still an issue that needs to be fixed.