More conservative value analysis of pointer equality

[xavierleroy]

Consider two global variables x and y. Currently, the value analysis considers that any pointer based on x cannot be equal to any pointer based on y. This reflects the CompCert C semantics for pointer equality: if the two pointers are within bounds, they must differ; and if one pointer is outside bounds (including if it is "one past"), comparison is undefined.

However, a pointer "one past" x and a pointer to the beginning of y can be equal at the machine level, and comparing them for equality is not undefined behavior in ISO C, just an unpredictable result.

This PR makes sure CompCert's value analysis says "I don't know" for equality tests between pointers based on different global variables. It still says "false or undefined" for equality between a pointer based in the current stack block and a pointer based elsewhere, as such pointers can never be equal even if "one past".

[xavierleroy]

Follow-up commit: fd48dc868