diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-05-30 12:27:15 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-05-30 12:27:15 +0000 |
| commit | f4b41226d60ca57c5981b0a46e0a495152b5301f (patch) | |
| tree | fb3ea7a1cabfc5e4c56ecc1b60eeacd2883a8293 /extraction | |
| parent | f77e0ade09d8fd17add98c3bc4317627078f3aa8 (diff) | |
Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore utilisee dans le front-end C.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/.depend | 13 | ||||
| -rw-r--r-- | extraction/extraction.v | 1 |
2 files changed, 9 insertions, 5 deletions
diff --git a/extraction/.depend b/extraction/.depend index d26acb9..4f6abc2 100644 --- a/extraction/.depend +++ b/extraction/.depend @@ -59,9 +59,9 @@ ../caml/PrintPPC.cmx: PPC.cmx Datatypes.cmx ../caml/Camlcoq.cmx CList.cmx \ AST.cmx ../caml/PrintPPC.cmi ../caml/RTLgenaux.cmo: Switch.cmi Integers.cmi Datatypes.cmi CminorSel.cmi \ - CList.cmi + ../caml/Camlcoq.cmo CList.cmi ../caml/RTLgenaux.cmx: Switch.cmx Integers.cmx Datatypes.cmx CminorSel.cmx \ - CList.cmx + ../caml/Camlcoq.cmx CList.cmx ../caml/RTLtypingaux.cmo: Registers.cmi RTL.cmi Op.cmi Maps.cmi Datatypes.cmi \ ../caml/Camlcoq.cmo CList.cmi AST.cmi ../caml/RTLtypingaux.cmx: Registers.cmx RTL.cmx Op.cmx Maps.cmx Datatypes.cmx \ @@ -191,7 +191,8 @@ Stacking.cmi: Specif.cmi Op.cmi Mach.cmi Locations.cmi Linear.cmi \ Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ CString.cmi CList.cmi Bounds.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi Sumbool.cmi: Specif.cmi Datatypes.cmi -Switch.cmi: Integers.cmi EqNat.cmi Datatypes.cmi CList.cmi +Switch.cmi: Specif.cmi Integers.cmi EqNat.cmi Datatypes.cmi Coqlib.cmi \ + CList.cmi BinPos.cmi BinInt.cmi Tunneling.cmi: Maps.cmi LTL.cmi Datatypes.cmi AST.cmi Values.cmi: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ BinPos.cmi BinInt.cmi AST.cmi @@ -490,8 +491,10 @@ Stacking.cmx: Specif.cmx Op.cmx Mach.cmx Locations.cmx Linear.cmx \ Stacking.cmi Sumbool.cmo: Specif.cmi Datatypes.cmi Sumbool.cmi Sumbool.cmx: Specif.cmx Datatypes.cmx Sumbool.cmi -Switch.cmo: Integers.cmi EqNat.cmi Datatypes.cmi CList.cmi Switch.cmi -Switch.cmx: Integers.cmx EqNat.cmx Datatypes.cmx CList.cmx Switch.cmi +Switch.cmo: Specif.cmi Integers.cmi EqNat.cmi Datatypes.cmi Coqlib.cmi \ + CList.cmi BinPos.cmi BinInt.cmi Switch.cmi +Switch.cmx: Specif.cmx Integers.cmx EqNat.cmx Datatypes.cmx Coqlib.cmx \ + CList.cmx BinPos.cmx BinInt.cmx Switch.cmi Tunneling.cmo: Maps.cmi LTL.cmi Datatypes.cmi AST.cmi Tunneling.cmi Tunneling.cmx: Maps.cmx LTL.cmx Datatypes.cmx AST.cmx Tunneling.cmi Values.cmo: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ diff --git a/extraction/extraction.v b/extraction/extraction.v index fc2920e..abb792c 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -30,6 +30,7 @@ Extract Constant Floats.Float.neg => "( ~-. )". Extract Constant Floats.Float.abs => "abs_float". Extract Constant Floats.Float.singleoffloat => "Floataux.singleoffloat". Extract Constant Floats.Float.intoffloat => "Floataux.intoffloat". +Extract Constant Floats.Float.intuoffloat => "Floataux.intuoffloat". Extract Constant Floats.Float.floatofint => "Floataux.floatofint". Extract Constant Floats.Float.floatofintu => "Floataux.floatofintu". Extract Constant Floats.Float.add => "( +. )". |