Avoid emitting reflexive pointer refines for locking

[sim642]

This is an alternative optimized fix for #1374.

This is extracted from the end of #1396.

[sim642]

This should work, but it seems to reveal some pre-existing issue in the relational atomic privatization stuff. Namely with the special [__VERIFIER_atomic] mutex variable used for that.

Quick tracing reveals something which definitely shouldn't be happening: the Apron environment contains a variable named [__VERIFIER_atomic]. This is because locking it and emitting a branch on &[__VERIFIER_atomic] == &[__VERIFIER_atomic] causes the relational analysis branch to read the global variable somehow. I guess because it happens to be a pointer to int, which [__VERIFIER_atomic]'s declared type. And that somehow changes everything.