analyzer Add explicit W set to base protection privatization

Regarding https://github.com/goblint/analyzer/pull/1636#discussion_r1963055883.

Surprisingly, there was even a TODO about it: https://github.com/goblint/analyzer/blob/a9354564fbb6b3d86879a4949f9d93c04399584c/src/analyses/basePriv.ml#L940-L943

Feb 20 '25 09:02 sim642

Hmm, I suppose keeping separate CPA maps for written and refined values could be more precise indeed. Although that doesn't seem like it should to be specific to Protection-Based Reading, but potentially all/many privatizations?

Mar 04 '25 18:03 sim642

Although that doesn't seem like it should to be specific to Protection-Based Reading, but potentially all/many privatizations?

Sure! I think for base we know that it pays off. Not sure whether it's worth adding it to all privatizations?

Mar 04 '25 19:03 michael-schwarz

To each one individually, probably not. I was thinking more along the lines of some kind of generic lifting with the dual CPAs or something. I don't have a specific idea though, so it might not really be possible so generally.

Mar 04 '25 21:03 sim642