diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 08:54:56 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 08:54:56 +0000 |
commit | 2a0168fea37b68ad14e2cb60bf215111e49d4870 (patch) | |
tree | 2f59373790d8ce3a5df66ef7a692271cf0666c6c /test/regression/NaNs.c | |
parent | 00805153cf9b88aa07cc6694b17d93f5ba2e7de8 (diff) | |
download | compcert-2a0168fea37b68ad14e2cb60bf215111e49d4870.tar.gz compcert-2a0168fea37b68ad14e2cb60bf215111e49d4870.zip |
Merge of "newspilling" branch:
- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
support saving and restoring registers without knowing
the exact types (int/single/float) of their contents, just
their sizes.
- Memory model: generalize the opaque encoding of pointers to
apply to any value, not just pointers, if chunks Many32/Many64
are selected.
- More properties of FP arithmetic proved.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'test/regression/NaNs.c')
-rw-r--r-- | test/regression/NaNs.c | 48 |
1 files changed, 42 insertions, 6 deletions
diff --git a/test/regression/NaNs.c b/test/regression/NaNs.c index 45f1e7fb..618ce295 100644 --- a/test/regression/NaNs.c +++ b/test/regression/NaNs.c @@ -32,17 +32,17 @@ inline float single_of_bits(u32 i) u.i = i; return u.f; } -volatile double val[8]; - char * valname[8] = { "+0", "-0", "+inf", "-inf", "snan(5)", "qnan(6)", "snan(-9)", "qnan(-1)" }; -int main() +void test64(void) { + volatile double val[8]; int i, j; + printf("--- Double precision\n"); val[0] = 0.0; val[1] = - val[0]; val[2] = double_of_bits(0x7FF0000000000000); @@ -56,10 +56,7 @@ int main() for (i = 0; i < 8; i++) { printf("opp(%s) = 0x%016llx\n", valname[i], bits_of_double(- val[i])); printf("single(%s) = 0x%08x\n", valname[i], bits_of_single((float)(val[i]))); -#if 0 - /* The reference interpreter doesn't support __builtin_fabs */ printf("abs(%s) = 0x%016llx\n", valname[i], bits_of_double(__builtin_fabs(val[i]))); -#endif for (j = 0; j < 8; j++) { printf("%s + %s = 0x%016llx\n", valname[i], valname[j], bits_of_double(val[i] + val[j])); @@ -71,5 +68,44 @@ int main() valname[i], valname[j], bits_of_double(val[i] / val[j])); } } +} + +void test32(void) +{ + volatile float val[8]; + int i, j; + + printf("--- Single precision\n"); + val[0] = 0.0f; + val[1] = - val[0]; + val[2] = single_of_bits(0x7F800000); + val[3] = - val[2]; + + val[4] = single_of_bits(0x7F800005); + val[5] = single_of_bits(0x7FC00006); + val[6] = single_of_bits(0xFF800009); + val[7] = single_of_bits(0xFFC00001); + + for (i = 0; i < 8; i++) { + printf("opp(%s) = 0x%08x\n", valname[i], bits_of_single(- val[i])); + printf("double(%s) = 0x%016llx\n", valname[i], bits_of_double((double)(val[i]))); + printf("abs(%s) = 0x%08x\n", valname[i], bits_of_single(__builtin_fabs(val[i]))); + for (j = 0; j < 8; j++) { + printf("%s + %s = 0x%08x\n", + valname[i], valname[j], bits_of_single(val[i] + val[j])); + printf("%s - %s = 0x%08x\n", + valname[i], valname[j], bits_of_single(val[i] - val[j])); + printf("%s * %s = 0x%08x\n", + valname[i], valname[j], bits_of_single(val[i] * val[j])); + printf("%s / %s = 0x%08x\n", + valname[i], valname[j], bits_of_single(val[i] / val[j])); + } + } +} + +int main(void) +{ + test64(); + test32(); return 0; } |