diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-11 09:41:30 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-11 09:41:30 +0000 |
commit | bd3e0f3a49e9f785dd75f2806bf791e3aa58b584 (patch) | |
tree | 63e6320ebc72da1f0143f49aeb822a8a16801d5c | |
parent | 7dd08351a9167f99c04f47042fb83c03e10d5552 (diff) |
Fixed parsing of hex float literals 0xNNNpMMM.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2144 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r-- | cfrontend/C2C.ml | 2 | ||||
-rw-r--r-- | test/c/Makefile | 4 | ||||
-rw-r--r-- | test/c/Results/floats-basics | 1 | ||||
-rw-r--r-- | test/c/bisect.c | 3 | ||||
-rw-r--r-- | test/c/floats-basics.c | 75 |
5 files changed, 81 insertions, 4 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index f34c396..f80b379 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -370,7 +370,7 @@ let convertFloat f kind = (if f.C.hex then 4 else 1) * String.length f.C.fracPart in let exp = Z.sub exp (Z.of_uint shift_exp) in - let base = P.of_int (if f.C.hex then 16 else 10) in + let base = P.of_int (if f.C.hex then 2 else 10) in begin match kind with | FFloat -> diff --git a/test/c/Makefile b/test/c/Makefile index f4d8f41..6839ac4 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -13,9 +13,9 @@ TIME=xtime -o /dev/null -mintime 1.0 # Xavier's hack PROGS=fib integr qsort fft sha1 aes almabench lists \ binarytrees fannkuch knucleotide mandelbrot nbody \ nsieve nsievebits spectral vmach \ - bisect chomp perlin floats + bisect chomp perlin floats floats-basics -PROGS_INTERP=floats +PROGS_INTERP=floats floats-basics all: $(PROGS:%=%.compcert) diff --git a/test/c/Results/floats-basics b/test/c/Results/floats-basics new file mode 100644 index 0000000..e5e16af --- /dev/null +++ b/test/c/Results/floats-basics @@ -0,0 +1 @@ +0 error(s) detected. diff --git a/test/c/bisect.c b/test/c/bisect.c index 759f997..14d0624 100644 --- a/test/c/bisect.c +++ b/test/c/bisect.c @@ -16,7 +16,8 @@ #include <stdlib.h> #include <string.h> #include <math.h> -#include <float.h> + +#define DBL_EPSILON 0x1p-52 void *allocvector(size_t size) { diff --git a/test/c/floats-basics.c b/test/c/floats-basics.c new file mode 100644 index 0000000..0a4c69d --- /dev/null +++ b/test/c/floats-basics.c @@ -0,0 +1,75 @@ +#include<stdio.h> +#include<stdlib.h> + +#define STR_EXPAND(tok) #tok +#define STR(tok) STR_EXPAND(tok) + +#if defined(__ppc__) || defined(__PPC__) +#define ARCH_BIG_ENDIAN +#elif defined(__i386__) || defined(__x86_64__) || defined(__ARMEL__) +#undef ARCH_BIG_ENDIAN +#else +#error "unknown endianness" +#endif + +union converter64 { + double dbl; + struct { +#ifdef ARCH_BIG_ENDIAN + unsigned h, l; +#else + unsigned l, h; +#endif + } u64; +}; + +int num_errors = 0; + +void comp64(double d, unsigned high, unsigned low, char* s) { + union converter64 c; + c.dbl = d; + if((c.u64.h & 0x7FF00000) == 0x7FF00000 && (c.u64.l | (c.u64.h & 0xFFFFF)) != 0) { + c.u64.l = 0xFFFFFFFF; + c.u64.h = 0x7FFFFFFF; + } + if((high & 0x7FF00000) == 0x7FF00000 && (low | (high & 0xFFFFF)) != 0) { + low = 0xFFFFFFFF; + high = 0x7FFFFFFF; + } + if(low != c.u64.l || high != c.u64.h) { + printf("%s : %08x %08x (%a)\n", s, c.u64.h, c.u64.l, d); + num_errors++; + } +} + +void compd(double d1, double d2, char* s) { + union converter64 c1, c2; + c1.dbl = d1; + c2.dbl = d2; + if(c1.u64.l != c2.u64.l || c1.u64.h != c2.u64.h) { + printf("%s : %a %a\n", s, d1, d2); + num_errors++; + } +} + +int main(void) { + comp64(3.518437208883201171875E+013, 0x42c00000, 0x00000002, STR(__LINE__)); + compd(1.50000000000000011102230246251565404236316680908203125, 0x1.8p+0, STR(__LINE__)); + compd(0.500000000000000166533453693773481063544750213623046875, 0x1.0000000000002p-1, STR(__LINE__)); + compd(1.2, 1.20000000000000005, STR(__LINE__)); + compd(1.2f, 1.2000001f, STR(__LINE__)); + compd(1, 1., STR(__LINE__)); + compd(0.5, .5, STR(__LINE__)); + compd(1, 1E0, STR(__LINE__)); + compd(0.5, 0x1p-1, STR(__LINE__)); + compd(0.5, 0x1.p-1, STR(__LINE__)); + compd(0.5, 0x.1p3, STR(__LINE__)); + compd(0.5, 0x.8p0, STR(__LINE__)); + compd(15./16, 0x.fp0, STR(__LINE__)); + compd(15./16, 0x.Fp0, STR(__LINE__)); + compd(15./16, 0x.fP0, STR(__LINE__)); + compd(15./16, 0X.fp0, STR(__LINE__)); + + printf("%d error(s) detected.\n", num_errors); + return 0; +} |