Vojdani privatization may output read-unprotected variables to witnesses

[sim642]

Both vojdani privatization:

analyzer/src/analyses/basePriv.ml

Line 857 in 66dff5a

let invariant_vars ask getg st = protected_vars ask

and protection privatization:

analyzer/src/analyses/basePriv.ml

Line 1061 in 66dff5a

let invariant_vars ask getg st = protected_vars ask

use the same implementation of invariant_vars:

analyzer/src/analyses/commonPriv.ml

Lines 102 to 106 in 66dff5a

	let protected_vars (ask: Q.ask): varinfo list =
	LockDomain.MustLockset.fold (fun ml acc ->
	Q.VS.join (ask.f (Q.MustProtectedVars {mutex = ml; write = true})) acc
	) (ask.f Q.MustLockset) (Q.VS.empty ())
	|> Q.VS.elements

This is weird, because one is built on read-write protection and the other just on write-protection.

I tried a small fix, but that revealed read-write protected variables being incorrectly computed (#1712). So this requires PR #1631 or something else that fixes the computation first.