The current implementation of symbolic lockset track sets of addresses known to be definitely equal to the address expressions that were used when locking. It relies on must-equalities to improve precision, but may-equality should be used when these sets are invalidated. When pointers are written to, it does seem like we rely on may information from the base analysis, but when mutexes are unlocked we do this based on the same must-eq query as for locking. This is unsound.

Additionally, we may want to extract some of the very semantic manipulations from the add/remove operations of the domain into the analysis. I'm not sure how normal it is for domain domains to do such value-dependent computations.

Test case was added for this in f3ba049.