From d71a5cfd10378301b71d32659d5936e01d72ae50 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 9 May 2010 08:18:51 +0000 Subject: Revised encoding/decoding of floats git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1341 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/extraction.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index e8fc572..797204f 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -42,11 +42,13 @@ Extract Constant Floats.Float.mul => "( *. )". Extract Constant Floats.Float.div => "( /. )". Extract Constant Floats.Float.cmp => "Floataux.cmp". Extract Constant Floats.Float.eq_dec => "fun (x: float) (y: float) -> x = y". +Extract Constant Floats.Float.bits_of_double => "Floataux.bits_of_double". +Extract Constant Floats.Float.double_of_bits => "Floataux.double_of_bits". +Extract Constant Floats.Float.bits_of_single => "Floataux.bits_of_single". +Extract Constant Floats.Float.single_of_bits => "Floataux.single_of_bits". (* Memdata *) Extract Constant Memdata.big_endian => "Memdataaux.big_endian". -Extract Constant Memdata.encode_float => "Memdataaux.encode_float". -Extract Constant Memdata.decode_float => "Memdataaux.decode_float". (* Memory - work around an extraction bug. *) Extraction NoInline Memory.Mem.valid_pointer. -- cgit v1.2.3