Merge of the reuse-temps branch:

- Reload temporaries are marked as destroyed (set to Vundef) across
  operations in the semantics of LTL, LTLin, Linear and Mach, 
  allowing Asmgen to reuse them.
- Added IA32 port.
- Cleaned up float conversions and axiomatization of floats.



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

10 files changed, 74 insertions, 36 deletions

diff --git a/test/c/Makefile b/test/c/Makefile
index b4fd1fd..7b6d63c 100644
--- a/test/c/Makefile
+++ b/test/c/Makefile
@@ -1,7 +1,7 @@
 include ../../Makefile.config
 
 CCOMP=../../ccomp
-CCOMPFLAGS=-stdlib ../../runtime -fmadd -dcmedium -dclight -dasm
+CCOMPFLAGS=-stdlib ../../runtime -fmadd -dc -dclight -dasm
 
 CFLAGS=-O1 -Wall
 
@@ -58,4 +58,4 @@ time_compcert:
 
 clean:
 	rm -f *.compcert *.gcc
-	rm -f *.light.c *.medium.c *.s *.o *~ 
+	rm -f *.light.c *.compcert.c *.s *.o *~ 
diff --git a/test/raytracer/Makefile b/test/raytracer/Makefile
index dea57af..8ba9ede 100644
--- a/test/raytracer/Makefile
+++ b/test/raytracer/Makefile
@@ -1,6 +1,8 @@
+include ../../Makefile.config
+
 CC=../../ccomp 
 CFLAGS=-stdlib ../../runtime -dparse -dclight -dasm -fstruct-passing -fstruct-assign
-LIBS=
+LIBS=$(LIBMATH)
 TIME=xtime -mintime 2.0
 
 OBJS=memory.o gmllexer.o gmlparser.o eval.o \
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 55b07f5..7d456df 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -1,12 +1,13 @@
 include ../../Makefile.config
 
 CCOMP=../../ccomp
-CCOMPFLAGS=-stdlib ../../runtime -dparse -dcmedium -dclight -dasm \
+CCOMPFLAGS=-stdlib ../../runtime -dparse -dc -dclight -dasm \
   -fstruct-passing -fstruct-assign -fbitfields
 
 LIBS=$(LIBMATH)
 
 # Can run and have reference output in Results
+
 TESTS=bitfields1 bitfields2 bitfields3 bitfields4 \
   bitfields5 bitfields6 \
   expr1 initializers volatile2 \
@@ -32,7 +33,7 @@ all: $(TESTS:%=%.compcert) $(EXTRAS:%=%.s)
 
 clean:
 	rm -f *.compcert
-	rm -f *.parsed.c *.light.c *.s *.o *~ 
+	rm -f *.parsed.c *.compcert.c *.light.c *.s *.o *~ 
 
 test:
 	@for i in $(TESTS); do \
diff --git a/test/regression/Results/casts3 b/test/regression/Results/casts3
new file mode 100644
index 0000000..78ee28a
--- /dev/null
+++ b/test/regression/Results/casts3
@@ -0,0 +1 @@
+........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
diff --git a/test/regression/Results/expr1 b/test/regression/Results/expr1
index dc49203..f5a6864 100644
--- a/test/regression/Results/expr1
+++ b/test/regression/Results/expr1
@@ -1 +1 @@
-Result: 0x0
+Result: 0
diff --git a/test/regression/casts3.c b/test/regression/casts3.c
new file mode 100644
index 0000000..f6e35c2
--- /dev/null
+++ b/test/regression/casts3.c
@@ -0,0 +1,60 @@
+/* Testing int <-> float conversions */
+
+#include <stdio.h>
+
+unsigned int urand(void)
+{
+  static unsigned int seed = 0;
+  seed = seed * 25173 + 8453;
+  return seed;
+}
+
+signed int srand(void)
+{
+  return (signed int) urand();
+}
+
+double fuzzing[] = { 0.0, 0.01, 0.25, 0.4, 0.5, 0.6, 0.75, 0.99 };
+
+double fuzz(void)
+{
+  static unsigned int n = 0;
+  n = n + 1;
+  if (n >= sizeof(fuzzing) / sizeof(double)) n = 0;
+  return fuzzing[n];
+}
+
+void test_signed_conv(void)
+{
+  int n = srand();
+  double f = fuzz();
+  double d = (double) n;
+  double e = n < 0 ? d - f : d + f;
+  int m = (int) e;
+  if (m != n)
+    printf("\nError: signed: %d, %g, %g, %d\n", n, f, e, m);
+}
+
+void test_unsigned_conv(void)
+{
+  unsigned int n = srand();
+  double f = fuzz();
+  double d = (double) n;
+  double e = f + d;
+  unsigned int m = (unsigned int) e;
+  if (m != n)
+    printf("\nError: unsigned: %u, %g, %g, %u\n", n, f, e, m);
+}
+
+int main()
+{
+  int i;
+  for (i = 0; i < 1000000; i++) {
+    if ((i % 1000) == 0) { printf("."); fflush(stdout); }
+    test_signed_conv();
+    test_unsigned_conv();
+  }
+  printf("\n");
+  return 0;
+}
+
diff --git a/test/regression/expr1.c b/test/regression/expr1.c
index 0cc7b54..132ce44 100644
--- a/test/regression/expr1.c
+++ b/test/regression/expr1.c
@@ -12,6 +12,6 @@ int main(int argc, char ** argv)
   struct list l;
   l.tl = &l;
   f(&(l.tl));
-  printf("Result: %p\n", l.tl);
+  printf("Result: %d\n", (int) l.tl);
   return 0;
 }
diff --git a/test/spass/Makefile b/test/spass/Makefile
index b964770..30832f8 100644
--- a/test/spass/Makefile
+++ b/test/spass/Makefile
@@ -1,3 +1,5 @@
+include ../../Makefile.config
+
 CC=../../ccomp 
 CFLAGS=-stdlib ../../runtime -dparse -dclight -dasm -fstruct-passing -fstruct-assign
 
@@ -13,7 +15,7 @@ SRCS=analyze.c clause.c clock.c closure.c cnf.c component.c                 \
 all: spass
 
 spass: $(SRCS:.c=.o)
-	$(CC) $(CFLAGS) -o spass $(SRCS:.c=.o)
+	$(CC) $(CFLAGS) -o spass $(SRCS:.c=.o) $(LIBMATH)
 
 clean:
 	rm -f spass
diff --git a/test/spass/dfgparser.c b/test/spass/dfgparser.c
index 3691271..b2bfa5d 100644
--- a/test/spass/dfgparser.c
+++ b/test/spass/dfgparser.c
@@ -359,20 +359,6 @@ typedef struct yyltype
 
 /* The parser invokes alloca or malloc; define the necessary symbols.  */
 
-# if YYSTACK_USE_ALLOCA
-#  define YYSTACK_ALLOC alloca
-# else
-#  ifndef YYSTACK_USE_ALLOCA
-#   if defined (alloca) || defined (_ALLOCA_H)
-#    define YYSTACK_ALLOC alloca
-#   else
-#    ifdef __GNUC__
-#     define YYSTACK_ALLOC __builtin_alloca
-#    endif
-#   endif
-#  endif
-# endif
-
 # ifdef YYSTACK_ALLOC
    /* Pacify GCC's `empty if-body' warning. */
 #  define YYSTACK_FREE(Ptr) do { /* empty */; } while (0)
diff --git a/test/spass/iaparser.c b/test/spass/iaparser.c
index 4fa8697..96274df 100644
--- a/test/spass/iaparser.c
+++ b/test/spass/iaparser.c
@@ -210,20 +210,6 @@ typedef struct yyltype
 
 /* The parser invokes alloca or malloc; define the necessary symbols.  */
 
-# if YYSTACK_USE_ALLOCA
-#  define YYSTACK_ALLOC alloca
-# else
-#  ifndef YYSTACK_USE_ALLOCA
-#   if defined (alloca) || defined (_ALLOCA_H)
-#    define YYSTACK_ALLOC alloca
-#   else
-#    ifdef __GNUC__
-#     define YYSTACK_ALLOC __builtin_alloca
-#    endif
-#   endif
-#  endif
-# endif
-
 # ifdef YYSTACK_ALLOC
    /* Pacify GCC's `empty if-body' warning. */
 #  define YYSTACK_FREE(Ptr) do { /* empty */; } while (0)