From 21aaf9c53b2bb0c6d376c2ce436d6dd7f5442a47 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 1 Feb 2021 18:53:04 +0100 Subject: bits to float --- riscV/SelectOp.vp | 2 ++ 1 file changed, 2 insertions(+) (limited to 'riscV/SelectOp.vp') diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp index 87e3af05..7714f12d 100644 --- a/riscV/SelectOp.vp +++ b/riscV/SelectOp.vp @@ -465,4 +465,6 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr match b with | BI_bits_of_float => Some (Eop Obits_of_single args) | BI_bits_of_double => Some (Eop Obits_of_float args) + | BI_float_of_bits => Some (Eop Osingle_of_bits args) + | BI_double_of_bits => Some (Eop Ofloat_of_bits args) end. \ No newline at end of file -- cgit