diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-09 08:18:51 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-09 08:18:51 +0000 |
| commit | d71a5cfd10378301b71d32659d5936e01d72ae50 (patch) | |
| tree | 9b6a7cc437ab205b7e0bf5bf90585451d8a8c367 /extraction | |
| parent | 913c1bcc4b2204afd447edd723e06b905fd1f47f (diff) | |
Revised encoding/decoding of floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1341 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 6 |
1 files changed, 4 insertions, 2 deletions
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. |