arm/PrintAsm: bugs in expansion of new builtins

test/: testing the builtins


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

1 files changed, 31 insertions, 14 deletions

diff --git a/test/regression/builtins.c b/test/regression/builtins.c
index b13578a..ea971bf 100644
--- a/test/regression/builtins.c
+++ b/test/regression/builtins.c
@@ -1,22 +1,22 @@
-/* Fun with PowerPC builtins */
+/* Fun with builtins */
 
 #include <stdio.h>
 
-#ifdef __ppc__
-
 int main(int argc, char ** argv)
 {
   int x = 0x12345678;
   unsigned int y = 0xDEADBEEF;
+  double a = 3.14159;
+  double b = 2.718;
+  double c = 1.414;
+  unsigned short s = 0x1234;
+
+#ifdef __ppc__
 
   printf("mulhw(%x, %x) = %x\n", x, y, __builtin_mulhw(x, y));
   printf("mulhwu(%x, %x) = %x\n", x, y, __builtin_mulhwu(x, y));
   printf("cntlzw(%x) = %d\n", x, __builtin_cntlzw(x));
 
-  double a = 3.14159;
-  double b = 2.718;
-  double c = 1.414;
-
   printf("fmadd(%f, %f, %f) = %f\n", a, b, c, __builtin_fmadd(a, b, c));
   printf("fmsub(%f, %f, %f) = %f\n", a, b, c, __builtin_fmsub(a, b, c));
   printf("fabs(%f) = %f\n", a, __builtin_fabs(a));
@@ -27,7 +27,30 @@ int main(int argc, char ** argv)
   printf("fsel(%f, %f, %f) = %f\n", a, b, c, __builtin_fsel(a, b, c));
   printf("fsel(%f, %f, %f) = %f\n", -a, b, c, __builtin_fsel(-a, b, c));
 
-  unsigned short s = 0x1234;
+  __builtin_eieio();
+  __builtin_sync();
+  __builtin_isync();
+
+#endif
+
+#ifdef __arm__
+
+  printf("bswap(%x) = %x\n", x, __builtin_bswap(x));
+
+  printf("fsqrt(%f) = %f\n", a, __builtin_fsqrt(a));
+  
+#endif
+
+#ifdef __i386__
+
+  printf("bswap(%x) = %x\n", x, __builtin_bswap(x));
+
+  printf("fsqrt(%f) = %f\n", a, __builtin_fsqrt(a));
+  printf("fmin(%f, %f) = %f\n", a, b, __builtin_fmin(a, b));
+  printf("fmax(%f, %f) = %f\n", a, b, __builtin_fmax(a, b));
+
+#endif
+
   printf ("read_16_rev = %x\n", __builtin_read_int16_reversed(&s));
   printf ("read_32_rev = %x\n", __builtin_read_int32_reversed(&y));
   __builtin_write_int16_reversed(&s, 0x789A);
@@ -35,15 +58,9 @@ int main(int argc, char ** argv)
   __builtin_write_int32_reversed(&y, 0x12345678);
   printf ("after write_32_rev: %x\n", y);
 
-  __builtin_eieio();
-  __builtin_sync();
-  __builtin_isync();
-
   return 0;
 }
 
-#endif
-