analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Reconsider not writing to known addresses if a pointer contains an unknown element

Open michael-schwarz opened this issue 1 year ago • 1 comments

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

michael-schwarz avatar May 14 '24 09:05 michael-schwarz

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.

sim642 avatar May 14 '24 09:05 sim642