From 5afebe369cea7f2746dec7c64514822562e9100e Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 11:22:59 +0100
Subject: begin synthesizing select

---
 riscV/SelectOp.vp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'riscV/SelectOp.vp')

diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index 7714f12d..0596ebf6 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -421,7 +421,11 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
 
 Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr)
    : option expr
-   := None.
+   := match ty with
+      | Tlong => Some (Eop Oselectl
+                       ((Eop (Ocmp cond) args) ::: e1 ::: e2 ::: Enil))
+      | _ => None
+      end.
  
 (** ** Recognition of addressing modes for load and store operations *)
 
-- 
cgit