From 5c84fd4adbcd8a63cc29fb0286cb46f18abde55c Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 29 Apr 2013 17:11:47 +0000 Subject: Expand 64-bit integer comparisons into 32-bit integer comparisons. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgen.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'cfrontend/Cshmgen.v') diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 3ab286e..c45e094 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -92,6 +92,8 @@ Definition make_cmp_ne_zero (e: expr) := | Ebinop (Ocmp c) e1 e2 => e | Ebinop (Ocmpu c) e1 e2 => e | Ebinop (Ocmpf c) e1 e2 => e + | Ebinop (Ocmpl c) e1 e2 => e + | Ebinop (Ocmplu c) e1 e2 => e | _ => Ebinop (Ocmp Cne) e (make_intconst Int.zero) end. -- cgit v1.2.3