modulos

1 files changed, 8 insertions, 0 deletions

diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp
index 72a6e4b3..089afe1d 100644
--- a/kvx/SelectOp.vp
+++ b/kvx/SelectOp.vp
@@ -762,6 +762,14 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr
                      | a:::b:::Enil => Some (FPDivision64.fp_divu64 a b)
                      | _ => None
                      end)
+  | BI_fp_umod32 => (match args with
+                     | a:::b:::Enil => Some (FPDivision32.fp_modu32 a b)
+                     | _ => None
+                     end)
+  | BI_fp_umod64 => (match args with
+                     | a:::b:::Enil => Some (FPDivision64.fp_modu64 a b)
+                     | _ => None
+                     end)
   end.
 End SELECT.