Simmo Saan

> The normal `HoareDomain.Set` just uses the default `Set` equality and probably just assumes that such sets are kept and compared only in their normal form. I guess `HoarePO` doesn't...

I suspect there's a reason why these operations have been implemented so inefficiently, address offsets don't actually have well-defined partitioning structure: https://github.com/goblint/analyzer/issues/101#issuecomment-1200996946.

Completed by #809.

A related point that arose during GobCon is that joining a thread multiple times is also undefined behavior.

Related to a couple of `*_unlocked` functions from the list, turns out there are `flockfile`, `ftrylockfile` and `funlockfile`, which treat a `FILE` as a mutex. No idea, if anyone uses...

Over time I've edited the issue and collected more domains that duplicate the Hoare ordering and operations to varying extents. I've been thinking hard about what a good (and not...

I got thinking about these things again to try to figure out the right generalization that captures both `AddressDomain` and `PathSensitive2`. As always happens when I touch this topic, I...

> Yes, but this on purpose here! Well, that depends on what the purpose exactly is. It would be equally reasonable to make it truly Hoare and keep them apart....

Having implemented general "Hoare" domains with pairwise and projected (e.g. by `hash`) joining strategies, it's now apparent that the joinability of addresses isn't a well-defined equivalence/partitioning at all. For example:...

The case I described can be fixed by joining anything (including a _must not zero_ index) with `NoOffset`. In order to make all offsets of a `varinfo` comparable, the second...