analyzer
analyzer copied to clipboard
Reconsider not writing to known addresses if a pointer contains an unknown element
We currently do completely ignore the possibility that any of the known pointers are written as soon as we have ? in the points-to set. This seems like it is philosophically the wrong thing to do to me.
In my opinion, we should at least potentially update the targets which we have identified.
https://github.com/goblint/analyzer/blob/a84e07d8780d5575ef90ad38cae51afde3964791/src/analyses/base.ml#L1730-L1748
I suspect the SetDomain.Unsupported code is some legacy thing that never even happens now. AddressSet.top isn't a lifted Top but a normal (foldable-over) set with UnknownPtr in it. And update_one there just ignores that one when doing Addr.to_mval.