PowerPC port: refactored the expansion of built-in functions and

pseudo-instructions so that it does not need to be re-done in
cchecklink.
cchecklink: updated accordingly.
testsuite: compile with -sdump and run cchecklink if supported.


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

6 files changed, 60 insertions, 5 deletions

diff --git a/test/Makefile b/test/Makefile
index 5771523..ab44be5 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -11,3 +11,6 @@ bench:
 
 clean:
 	for i in $(DIRS); do $(MAKE) -C $$i clean; done
+
+ccheck:
+	for i in $(DIRS); do $(MAKE) -C $$i ccheck; done
diff --git a/test/c/Makefile b/test/c/Makefile
index 1486666..a81a9d5 100644
--- a/test/c/Makefile
+++ b/test/c/Makefile
@@ -2,6 +2,10 @@ include ../../Makefile.config
 
 CCOMP=../../ccomp
 CCOMPFLAGS=-stdlib ../../runtime -dc -dclight -dasm
+ifeq ($(CCHECKLINK),true)
+CCHECK=../../cchecklink
+CCOMPFLAGS+= -sdump
+endif
 
 CFLAGS=-O1 -Wall
 
@@ -38,6 +42,12 @@ test:
 	   fi; \
          done
 
+ccheck:
+	@for i in $(PROGS); do \
+           echo "---- $$i"; \
+           $(CCHECK) -exe $$i.compcert $$i.sdump; \
+         done
+
 test_gcc:
 	@for i in $(PROGS); do \
 	   if ./$$i.gcc | cmp -s - Results/$$i; \
@@ -69,4 +79,4 @@ cminor_roundtrip:
 
 clean:
 	rm -f *.compcert *.gcc
-	rm -f *.compcert.c *.light.c *.parsed.c *.s *.o *~ 
+	rm -f *.compcert.c *.light.c *.parsed.c *.s *.o *.sdump *~ 
diff --git a/test/compression/Makefile b/test/compression/Makefile
index 8db55dd..e35e1a1 100644
--- a/test/compression/Makefile
+++ b/test/compression/Makefile
@@ -1,7 +1,13 @@
+include ../../Makefile.config
+
 CC=../../ccomp 
 CFLAGS=-U__GNUC__ -stdlib ../../runtime -dclight -dasm
 LIBS=
 TIME=xtime -o /dev/null -mintime 1.0
+ifeq ($(CCHECKLINK),true)
+CCHECK=../../cchecklink
+CFLAGS+= -sdump
+endif
 
 EXE=arcode lzw lzss
 
@@ -51,10 +57,18 @@ bench:
          done
 	rm -f $(TESTCOMPR)
 
+ccheck:
+	@echo "---- arcode"
+	@$(CCHECK) -exe arcode $(ARCODE_OBJS:.o=.sdump)
+	@echo "---- lzw"
+	@$(CCHECK) -exe lzw $(LZW_OBJS:.o=.sdump)
+	@echo "---- lzss"
+	@$(CCHECK) -exe lzss $(LZSS_OBJS:.o=.sdump)
+
 include .depend
 
 clean:
-	rm -f *.o *.light.c *.s $(EXE)
+	rm -f *.o *.light.c *.s *.sdump $(EXE)
 
 depend:
 	gcc -MM *.c > .depend
diff --git a/test/raytracer/Makefile b/test/raytracer/Makefile
index a4b8894..c6eb190 100644
--- a/test/raytracer/Makefile
+++ b/test/raytracer/Makefile
@@ -4,6 +4,10 @@ CC=../../ccomp
 CFLAGS=-stdlib ../../runtime -dparse -dclight -dasm -fstruct-return
 LIBS=$(LIBMATH)
 TIME=xtime -mintime 2.0
+ifeq ($(CCHECKLINK),true)
+CCHECK=../../cchecklink
+CFLAGS+= -sdump
+endif
 
 OBJS=memory.o gmllexer.o gmlparser.o eval.o \
   arrays.o vector.o matrix.o object.o intersect.o surface.o light.o \
@@ -15,7 +19,7 @@ render: $(OBJS)
 	$(CC) $(CFLAGS) -o render $(OBJS) $(LIBS)
 
 clean:
-	rm -f *.o *.parsed.c *.light.c *.s *.ppm render
+	rm -f *.o *.parsed.c *.light.c *.s *.sdump *.ppm render
 
 include .depend
 
@@ -55,3 +59,8 @@ test:
 
 bench:
 	@echo -n "raytracer: "; $(TIME) ./render < kal.gml
+
+ccheck:
+	@echo "---- render"
+	@$(CCHECK) -exe render *.sdump
+
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 189dbd8..3583676 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -2,6 +2,10 @@ include ../../Makefile.config
 
 CCOMP=../../ccomp
 CCOMPFLAGS=-stdlib ../../runtime -dparse -dc -dclight -dasm -fall
+ifeq ($(CCHECKLINK),true)
+CCHECK=../../cchecklink
+CCOMPFLAGS+= -sdump
+endif
 
 LIBS=$(LIBMATH)
 
@@ -48,7 +52,7 @@ all_s: $(TESTS:%=%.s) $(TESTS_COMP:%=%.s) $(TESTS_DIFF:%=%.s) $(EXTRAS:%=%.s)
 
 clean:
 	rm -f *.compcert
-	rm -f *.parsed.c *.compcert.c *.light.c *.s *.o *~ 
+	rm -f *.parsed.c *.compcert.c *.light.c *.s *.o *.sdump *~ 
 
 test:
 	@for i in $(TESTS) $(TESTS_COMP); do \
@@ -81,3 +85,10 @@ test:
          done
 
 bench:
+
+ccheck:
+	@for i in $(TESTS) $(TESTS_COMP); do \
+           echo "---- $$i"; \
+           $(CCHECK) -exe $$i.compcert $$i.sdump; \
+         done
+
diff --git a/test/spass/Makefile b/test/spass/Makefile
index 6797475..6a4cd59 100644
--- a/test/spass/Makefile
+++ b/test/spass/Makefile
@@ -2,6 +2,10 @@ include ../../Makefile.config
 
 CC=../../ccomp 
 CFLAGS=-stdlib ../../runtime -dparse -dclight -dasm -fstruct-return
+ifeq ($(CCHECKLINK),true)
+CCHECK=../../cchecklink
+CFLAGS+= -sdump
+endif
 
 SRCS=analyze.c clause.c clock.c closure.c cnf.c component.c                 \
   condensing.c context.c defs.c dfgparser.c dfgscanner.c doc-proof.c        \
@@ -19,7 +23,7 @@ spass: $(SRCS:.c=.o)
 
 clean:
 	rm -f spass
-	rm -f *.o *.s *.parsed.c *.light.c
+	rm -f *.o *.s *.parsed.c *.light.c *.sdump
 
 test:
 	./spass small_problem.dfg | grep 'Proof found'
@@ -30,6 +34,10 @@ TIME=xtime -o /dev/null     # Xavier's hack
 bench:
 	@echo -n "spass: "; $(TIME) ./spass problem.dfg
 
+ccheck:
+	@echo "---- spass"
+	@$(CCHECK) -exe spass *.sdump
+
 depend:
 	gcc -MM $(SRCS) > .depend