From 0f919eb26c68d3882e612a1b3a9df45bee6d3624 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 13 Feb 2019 18:53:17 +0100 Subject: Upgrade embedded version of Flocq to 3.1. Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully). --- Makefile | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 0247b688..5a9701aa 100644 --- a/Makefile +++ b/Makefile @@ -22,8 +22,8 @@ ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) endif DIRS=lib common $(ARCHDIRS) backend cfrontend driver \ - flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight \ - cparser cparser/MenhirLib + flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 \ + exportclight cparser cparser/MenhirLib RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight cparser @@ -43,15 +43,12 @@ GPATH=$(DIRS) # Flocq FLOCQ=\ - Fcore_Raux.v Fcore_Zaux.v Fcore_defs.v Fcore_digits.v \ - Fcore_float_prop.v Fcore_FIX.v Fcore_FLT.v Fcore_FLX.v \ - Fcore_FTZ.v Fcore_generic_fmt.v Fcore_rnd.v Fcore_rnd_ne.v \ - Fcore_ulp.v Fcore.v \ - Fcalc_bracket.v Fcalc_digits.v Fcalc_div.v Fcalc_ops.v \ - Fcalc_round.v Fcalc_sqrt.v \ - Fprop_div_sqrt_error.v Fprop_mult_error.v Fprop_plus_error.v \ - Fprop_relative.v Fprop_Sterbenz.v \ - Fappli_rnd_odd.v Fappli_double_round.v Fappli_IEEE.v Fappli_IEEE_bits.v + Raux.v Zaux.v Defs.v Digits.v Float_prop.v FIX.v FLT.v FLX.v FTZ.v \ + Generic_fmt.v Round_pred.v Round_NE.v Ulp.v Core.v \ + Bracket.v Div.v Operations.v Round.v Sqrt.v \ + Div_sqrt_error.v Mult_error.v Plus_error.v \ + Relative.v Sterbenz.v Round_odd.v Double_rounding.v \ + Binary.v Bits.v # General-purpose libraries (in lib/) -- cgit