`MayPointTo` is not subset of `ReachableFrom`

[sim642]

In #1174 I made pthread_join invalidate its second argument with w instead of the default r_deep; w_deep; s_deep. Surprisingly, this caused test failures due to additional unknown pointer accesses if the pthread_join argument happens to be NULL. This means that the MayPointTo for w accesses returns more addresses than ReachableFrom for w_deep, although I've always thought the former should be a subset of the latter as the latter is a recursive closure of the former. But apparently not?!

First, ReachableFrom for some reason excludes unknown pointers: https://github.com/goblint/analyzer/blob/851c6b3568de6d6ce51aeb06f771a7f8bd53cf64/src/analyses/base.ml#L1288-L1290 Second, reachable_from_value for some reason excludes NULL pointers: https://github.com/goblint/analyzer/blob/851c6b3568de6d6ce51aeb06f771a7f8bd53cf64/src/analyses/base.ml#L523 This explains why ReachableFrom NULL doesn't yield any accesses, but it doesn't explain why those exclusions are there in the first place.

In https://github.com/goblint/analyzer/pull/223/commits/a4fb6214961ba63f16e268eba6e26fd94b30505c reachable_from_value was not just moved around but also the AD.remove Addr.NullPtr was introduced without explanation.

[sim642]

There's also a third difference which affects NULL constants in particular because they evaluate to Int variants in base. MayPointTo returns the top pointer for them: https://github.com/goblint/analyzer/blob/851c6b3568de6d6ce51aeb06f771a7f8bd53cf64/src/analyses/base.ml#L1273 But ReachableFrom returns an empty points-to set: https://github.com/goblint/analyzer/blob/851c6b3568de6d6ce51aeb06f771a7f8bd53cf64/src/analyses/base.ml#L1291