From 72c5d592af9c9c0b417becc6abe5c2364d81639a Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 30 May 2008 14:28:57 +0000
Subject: Revu les comparaisons de pointeurs: == et <> sont definis entre 2
 pointeurs vers des blocs differents!

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@649 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/Csem.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'cfrontend/Csem.v')

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 35d3cce7..871f8831 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -292,7 +292,7 @@ Function sem_cmp (c:comparison)
           && valid_pointer m b2 (Int.signed ofs2) then
             if zeq b1 b2
             then Some (Val.of_bool (Int.cmp c ofs1 ofs2))
-            else None
+            else sem_cmp_mismatch c
           else None
       | Vptr b ofs, Vint n =>
           if Int.eq n Int.zero then sem_cmp_mismatch c else None
-- 
cgit