analyzer
analyzer copied to clipboard
Try to fix lval lattice
This is an attempt to address https://github.com/goblint/analyzer/issues/101#issuecomment-1200996946 and https://github.com/goblint/analyzer/pull/809#discussion_r935693299 by adding more lval lattice tests for some possibly reasonable structure and getting them to pass.
I've opened this separate from #809 because with the growing complexity and nuance of the domain, I'm no longer sure what the intended behavior should be. Right now I have added a bunch of extra cases to treat a
, a[0]
and a.fst
(first field) equivalently.
One can imagine increasingly complex lvals that this doesn't treat correctly. For example, a.snd
(second field) and a[0].snd
are the same memory location, but we don't currently treat them as equivalent, because the above equivalence is only ever applied at the end of the offset, not at every intermediate offset. I suspect the only way to deal with that would be to compute some edit distance between the offsets (i.e. where [0]
and .fst
can be inserted or removed to get from one to the other), but that would be insane. I guess this is why some people use automata to describe access paths...