Take advantage of Cmaskzero and Cmasknotzero.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1825 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 7 insertions, 0 deletions

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.