fpdivu

1 files changed, 6 insertions, 0 deletions

diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp
index f529907d..70941c48 100644
--- a/kvx/SelectOp.vp
+++ b/kvx/SelectOp.vp
@@ -742,6 +742,8 @@ Nondetfunction gen_fmaf args :=
   | _ => None
   end.
 
+Require FPDivision32.
+
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
   match b with
   | BI_fmin => Some (Eop Ominf args)
@@ -752,6 +754,10 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr
   | BI_fmaf => gen_fmaf args
   | BI_lround_ne => Some (Eop Olongoffloat_ne args)
   | BI_luround_ne => Some (Eop Olonguoffloat_ne args)
+  | BI_fp_udiv32 => (match args with
+                     | a:::b:::Enil => Some (FPDivision32.fp_divu32 a b)
+                     | _ => None
+                     end)
   end.
 End SELECT.