Unsound base privatizations after pruning

[sim642]

During benchmarking I found out that some base privatizations can be unsound during witness validation. I've added the following skipped test: https://github.com/goblint/analyzer/blob/e934d115271b7ae4b15e2d25edcf5e22dbcdb7ca/tests/regression/56-witness/04-base-priv-sync-prune.c. The invariant g == 2 should definitely fail, but if run, write+lock currently outputs that it holds. The same issue occurs with write and lock privatizations separately.

The problem is that these privatizations don't implement sync Join for publishing anything on branched thread creation, but every thread creation loop is a branched thread creation in disguise! It isn't a problem during the analysis itself, but the postsolving reachability pass never sees enter_multithreaded, so the initial global values are not side-effected and hence are considered unreachable. They are then removed from the solution and when witness validation performs an EvalInt query containing a default bot value, the whole expression comes out as bot, which is the same as if the program point was dead (and the invariant isn't violated).

Therefore these privatizations must also implement sync Join (where there currently are questioning TODOs) in order for the pruned solution to still be sound.

[sim642]

By the way c44f9cabbb434406870fa13350ec045484878363 from #770 accidentally works around the unsoundness issue by making the bot-valued variable expression have a top value instead. That is how I stumbled upon the issue: #770 seemed to make some benchmarks with write+lock less precise and turns out it worked around this unsoundness.

Even with #770 in place this should be fixed, since that makes write+lock output unknown about the invariant, while protection can output that it definitely fails.