From 62316a8e94d8cdcbf9e7aeadd1caf8e29507e6b0 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 24 Feb 2012 16:43:38 +0000
Subject: Take advantage of Cmaskzero and Cmasknotzero.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1825 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 ia32/SelectOp.vp | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'ia32/SelectOp.vp')

diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index 98db388..62de4ce 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -429,3 +429,10 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   | _ => (Aindexed Int.zero, e:::Enil)
   end.
 
+(** ** Turning an expression into a condition *)
+
+Nondetfunction cond_of_expr (e: expr) :=
+  match e with
+  | Eop (Oandimm n) (t1:::Enil) => (Cmasknotzero n, t1:::Enil)
+  | _ => (Ccompuimm Cne Int.zero, e:::Enil)
+  end.
-- 
cgit v1.2.3