Return Btop for undefined pointer comparisons in non-strict mode

Comparing pointers from different blocks with `< <= > >=`
is undefined behavior in CompCert and in ISO C.  So, it is sound to
analyze such comparisons as `Bnone`.

However, these comparisons occur in real code, and produce
statically-unpredictable Boolean results, so it is safer and more
consistent with other parts of the value analysis to return `Btop` in
non-strict mode.

Currently, this should make no difference to the generated code, since
CompCert does not optimize based on the absence of undefined
comparisons.

Author: xavierleroy

backend/ValueDomain.v

@@ -373,19 +373,19 @@ Definition cmp_different_blocks (c: comparison) : abool :=
   match c with
   | Ceq => Maybe false
   | Cne => Maybe true
-  | _   => Bnone
+  | _   => if va_strict tt then Bnone else Btop
   end.
 
 Lemma cmp_different_blocks_none:
   forall c, cmatch None (cmp_different_blocks c).
 Proof.
-  intros; destruct c; constructor.
+  unfold cmp_different_blocks. destruct c, (va_strict tt); constructor.
 Qed.
 
 Lemma cmp_different_blocks_sound:
   forall c, cmatch (Val.cmp_different_blocks c) (cmp_different_blocks c).
 Proof.
-  intros; destruct c; constructor.
+  unfold cmp_different_blocks. destruct c, (va_strict tt); constructor.
 Qed.
 
 Definition pcmp (c: comparison) (p1 p2: aptr) : abool :=