Use Flocq for floats

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 29 insertions, 2 deletions

diff --git a/.depend b/.depend
index 5cc392f..df0d874 100644
--- a/.depend
+++ b/.depend
@@ -7,7 +7,7 @@ lib/Lattice.vo lib/Lattice.glob: lib/Lattice.v lib/Coqlib.vo lib/Maps.vo
 lib/Ordered.vo lib/Ordered.glob: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo
 lib/Iteration.vo lib/Iteration.glob: lib/Iteration.v lib/Axioms.vo lib/Coqlib.vo lib/Wfsimpl.vo
 lib/Integers.vo lib/Integers.glob: lib/Integers.v lib/Axioms.vo lib/Coqlib.vo
-lib/Floats.vo lib/Floats.glob: lib/Floats.v lib/Coqlib.vo lib/Integers.vo
+lib/Floats.vo lib/Floats.glob: lib/Floats.v lib/Axioms.vo lib/Coqlib.vo lib/Integers.vo flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE_bits.vo flocq/Core/Fcore.vo
 lib/Parmov.vo lib/Parmov.glob: lib/Parmov.v lib/Axioms.vo lib/Coqlib.vo
 lib/UnionFind.vo lib/UnionFind.glob: lib/UnionFind.v lib/Coqlib.vo
 lib/Wfsimpl.vo lib/Wfsimpl.glob: lib/Wfsimpl.v lib/Axioms.vo
@@ -52,7 +52,7 @@ backend/Constpropproof.vo backend/Constpropproof.glob: backend/Constpropproof.v
 $(ARCH)/CombineOp.vo $(ARCH)/CombineOp.glob: $(ARCH)/CombineOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo $(ARCH)/SelectOp.vo
 backend/CSE.vo backend/CSE.glob: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo $(ARCH)/CombineOp.vo
 $(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob: $(ARCH)/CombineOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/CombineOp.vo backend/CSE.vo
-backend/CSEproof.vo backend/CSEproof.glob: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/CSE.vo
+backend/CSEproof.vo backend/CSEproof.glob: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOpproof.vo backend/CSE.vo
 $(ARCH)/Machregs.vo $(ARCH)/Machregs.glob: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo
 backend/Locations.vo backend/Locations.glob: backend/Locations.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo
 $(ARCH)/$(VARIANT)/Conventions1.vo $(ARCH)/$(VARIANT)/Conventions1.glob: $(ARCH)/$(VARIANT)/Conventions1.v lib/Coqlib.vo common/AST.vo backend/Locations.vo
@@ -115,3 +115,30 @@ cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob: cfrontend/Cminorgen.v lib/Coqli
 cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo
 driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Cexec.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo backend/Machsem.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/Inlining.vo backend/Renumber.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Reload.vo backend/RRE.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/Inliningproof.vo backend/Renumberproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/CleanupLabelsproof.vo backend/CleanupLabelstyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/RREproof.vo backend/RREtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo $(ARCH)/Asmgenproof.vo
 driver/Complements.vo driver/Complements.glob: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo backend/Cminor.vo backend/RTL.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo
+flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_float_prop.glob: flocq/Core/Fcore_float_prop.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo
+flocq/Core/Fcore_Zaux.vo flocq/Core/Fcore_Zaux.glob: flocq/Core/Fcore_Zaux.v
+flocq/Core/Fcore_rnd_ne.vo flocq/Core/Fcore_rnd_ne.glob: flocq/Core/Fcore_rnd_ne.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_ulp.vo
+flocq/Core/Fcore_FTZ.vo flocq/Core/Fcore_FTZ.glob: flocq/Core/Fcore_FTZ.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_FLX.vo
+flocq/Core/Fcore_FLT.vo flocq/Core/Fcore_FLT.glob: flocq/Core/Fcore_FLT.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_FLX.vo flocq/Core/Fcore_FIX.vo flocq/Core/Fcore_rnd_ne.vo
+flocq/Core/Fcore_defs.vo flocq/Core/Fcore_defs.glob: flocq/Core/Fcore_defs.v flocq/Core/Fcore_Raux.vo
+flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_Raux.glob: flocq/Core/Fcore_Raux.v flocq/Core/Fcore_Zaux.vo
+flocq/Core/Fcore_ulp.vo flocq/Core/Fcore_ulp.glob: flocq/Core/Fcore_ulp.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_float_prop.vo
+flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_rnd.glob: flocq/Core/Fcore_rnd.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo
+flocq/Core/Fcore_FLX.vo flocq/Core/Fcore_FLX.glob: flocq/Core/Fcore_FLX.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_FIX.vo flocq/Core/Fcore_rnd_ne.vo
+flocq/Core/Fcore_FIX.vo flocq/Core/Fcore_FIX.glob: flocq/Core/Fcore_FIX.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_rnd_ne.vo
+flocq/Core/Fcore_digits.vo flocq/Core/Fcore_digits.glob: flocq/Core/Fcore_digits.v flocq/Core/Fcore_Zaux.vo
+flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_generic_fmt.glob: flocq/Core/Fcore_generic_fmt.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_float_prop.vo
+flocq/Core/Fcore.vo flocq/Core/Fcore.glob: flocq/Core/Fcore.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_rnd_ne.vo flocq/Core/Fcore_FIX.vo flocq/Core/Fcore_FLX.vo flocq/Core/Fcore_FLT.vo flocq/Core/Fcore_ulp.vo
+flocq/Prop/Fprop_Sterbenz.vo flocq/Prop/Fprop_Sterbenz.glob: flocq/Prop/Fprop_Sterbenz.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_generic_fmt.vo flocq/Calc/Fcalc_ops.vo
+flocq/Prop/Fprop_mult_error.vo flocq/Prop/Fprop_mult_error.glob: flocq/Prop/Fprop_mult_error.v flocq/Core/Fcore.vo flocq/Calc/Fcalc_ops.vo
+flocq/Prop/Fprop_relative.vo flocq/Prop/Fprop_relative.glob: flocq/Prop/Fprop_relative.v flocq/Core/Fcore.vo
+flocq/Prop/Fprop_div_sqrt_error.vo flocq/Prop/Fprop_div_sqrt_error.glob: flocq/Prop/Fprop_div_sqrt_error.v flocq/Core/Fcore.vo flocq/Calc/Fcalc_ops.vo flocq/Prop/Fprop_relative.vo
+flocq/Prop/Fprop_plus_error.vo flocq/Prop/Fprop_plus_error.glob: flocq/Prop/Fprop_plus_error.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_generic_fmt.vo flocq/Calc/Fcalc_ops.vo
+flocq/Calc/Fcalc_ops.vo flocq/Calc/Fcalc_ops.glob: flocq/Calc/Fcalc_ops.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo
+flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_bracket.glob: flocq/Calc/Fcalc_bracket.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo
+flocq/Calc/Fcalc_sqrt.vo flocq/Calc/Fcalc_sqrt.glob: flocq/Calc/Fcalc_sqrt.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_digits.vo flocq/Core/Fcore_float_prop.vo flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_digits.vo
+flocq/Calc/Fcalc_div.vo flocq/Calc/Fcalc_div.glob: flocq/Calc/Fcalc_div.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_digits.vo
+flocq/Calc/Fcalc_round.vo flocq/Calc/Fcalc_round.glob: flocq/Calc/Fcalc_round.v flocq/Core/Fcore.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_digits.vo
+flocq/Calc/Fcalc_digits.vo flocq/Calc/Fcalc_digits.glob: flocq/Calc/Fcalc_digits.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_digits.vo
+flocq/Appli/Fappli_IEEE_bits.vo flocq/Appli/Fappli_IEEE_bits.glob: flocq/Appli/Fappli_IEEE_bits.v flocq/Core/Fcore.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_digits.vo flocq/Appli/Fappli_IEEE.vo
+flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE.glob: flocq/Appli/Fappli_IEEE.v flocq/Core/Fcore.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_digits.vo flocq/Calc/Fcalc_round.vo flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_ops.vo flocq/Calc/Fcalc_div.vo flocq/Calc/Fcalc_sqrt.vo flocq/Prop/Fprop_relative.vo