Merge remote-tracking branch 'origin/mppa-work' into mppa-duplicate-oracle

7 files changed, 187 insertions, 42 deletions

diff --git a/test/mppa/check.sh b/test/mppa/check.sh
deleted file mode 100755
index f25c3e31..00000000
--- a/test/mppa/check.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/bash
-# Tests the execution of the binaries produced by CompCert
-
-source do_test.sh
-
-do_test check $1
diff --git a/test/mppa/hardcheck.sh b/test/mppa/hardcheck.sh
new file mode 100755
index 00000000..82b63182
--- /dev/null
+++ b/test/mppa/hardcheck.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+# Tests the execution of the binaries produced by CompCert, in hardware
+
+source do_test.sh
+
+do_test hardcheck
diff --git a/test/mppa/hardtest.sh b/test/mppa/hardtest.sh
new file mode 100755
index 00000000..09511da6
--- /dev/null
+++ b/test/mppa/hardtest.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+# Tests the validity of the tests, in hardware
+
+source do_test.sh
+
+do_test hardtest
diff --git a/test/mppa/instr/Makefile b/test/mppa/instr/Makefile
index 69446796..37f7d0ab 100644
--- a/test/mppa/instr/Makefile
+++ b/test/mppa/instr/Makefile
@@ -5,10 +5,11 @@ CC ?= gcc
 CCOMP ?= ccomp
 OPTIM ?= -O2
 CFLAGS ?= $(OPTIM)
-CCOMPFLAGS ?= $(CFLAGS) -faddx
+CCOMPFLAGS ?= $(CFLAGS)
 SIMU ?= k1-mppa
 TIMEOUT ?= --signal=SIGTERM 120s
 DIFF ?= python2.7 floatcmp.py -reltol .00001
+HARDRUN ?= k1-jtag-runner
 
 DIR=./
 SRCDIR=$(DIR)
@@ -30,10 +31,11 @@ SIMUPATH=$(shell which $(SIMU))
 
 TESTNAMES?=$(notdir $(subst .c,,$(wildcard $(DIR)/*.c)))
 X86_GCC_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .x86-gcc.out,$(TESTNAMES)))
-GCC_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.out,$(TESTNAMES)))
-CCOMP_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.out,$(TESTNAMES)))
+GCC_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.simu.out,$(TESTNAMES)))
+CCOMP_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.simu.out,$(TESTNAMES)))
+GCC_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.hard.out,$(TESTNAMES)))
+CCOMP_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.hard.out,$(TESTNAMES)))
 
-OUT=$(X86_GCC_OUT) $(GCC_OUT) $(CCOMP_OUT)
 BIN=$(addprefix $(BINDIR)/,$(addsuffix .x86-gcc.bin,$(TESTNAMES)))\
 	$(addprefix $(BINDIR)/,$(addsuffix .gcc.bin,$(TESTNAMES)))\
 	$(addprefix $(BINDIR)/,$(addsuffix .ccomp.bin,$(TESTNAMES)))
@@ -49,12 +51,18 @@ RED=\033[0;31m
 YELLOW=\033[0;33m
 NC=\033[0m
 
+.PHONY:
+test: simutest
+
+.PHONY:
+check: simucheck
+
 .PHONY: 
-test: $(X86_GCC_OUT) $(GCC_OUT)
+simutest: $(X86_GCC_OUT) $(GCC_SIMUOUT)
 	@echo "Comparing x86 gcc output to k1 gcc.."
 	for test in $(TESTNAMES); do\
 		x86out=$(OUTDIR)/$$test.x86-gcc.out;\
-		gccout=$(OUTDIR)/$$test.gcc.out;\
+		gccout=$(OUTDIR)/$$test.gcc.simu.out;\
 		if grep "__K1C__" -q $$test.c; then\
 			printf "$(YELLOW)UNTESTED: $$test.c contains an \`#ifdef __K1C__\`\n";\
 		elif $(DIFF) $$x86out $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\
@@ -65,11 +73,39 @@ test: $(X86_GCC_OUT) $(GCC_OUT)
 	done
 
 .PHONY:
-check: $(GCC_OUT) $(CCOMP_OUT)
+simucheck: $(GCC_SIMUOUT) $(CCOMP_SIMUOUT)
 	@echo "Comparing k1 gcc output to ccomp.."
 	@for test in $(TESTNAMES); do\
-		gccout=$(OUTDIR)/$$test.gcc.out;\
-		ccompout=$(OUTDIR)/$$test.ccomp.out;\
+		gccout=$(OUTDIR)/$$test.gcc.simu.out;\
+		ccompout=$(OUTDIR)/$$test.ccomp.simu.out;\
+		if $(DIFF) $$ccompout $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\
+			>&2 printf "$(RED)ERROR: $$ccompout and $$gccout differ$(NC)\n";\
+		else\
+			printf "$(GREEN)GOOD: $$ccompout and $$gccout concur$(NC)\n";\
+		fi;\
+	done
+
+.PHONY: 
+hardtest: $(X86_GCC_OUT) $(GCC_HARDOUT)
+	@echo "Comparing x86 gcc output to k1 gcc.."
+	for test in $(TESTNAMES); do\
+		x86out=$(OUTDIR)/$$test.x86-gcc.out;\
+		gccout=$(OUTDIR)/$$test.gcc.hard.out;\
+		if grep "__K1C__" -q $$test.c; then\
+			printf "$(YELLOW)UNTESTED: $$test.c contains an \`#ifdef __K1C__\`\n";\
+		elif $(DIFF) $$x86out $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\
+			>&2 printf "$(RED)ERROR: $$x86out and $$gccout differ$(NC)\n";\
+		else\
+			printf "$(GREEN)GOOD: $$x86out and $$gccout concur$(NC)\n";\
+		fi;\
+	done
+
+.PHONY:
+hardcheck: $(GCC_HARDOUT) $(CCOMP_HARDOUT)
+	@echo "Comparing k1 gcc output to ccomp.."
+	@for test in $(TESTNAMES); do\
+		gccout=$(OUTDIR)/$$test.gcc.hard.out;\
+		ccompout=$(OUTDIR)/$$test.ccomp.hard.out;\
 		if $(DIFF) $$ccompout $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\
 			>&2 printf "$(RED)ERROR: $$ccompout and $$gccout differ$(NC)\n";\
 		else\
@@ -95,14 +131,22 @@ $(OUTDIR)/%.x86-gcc.out: $(BINDIR)/%.x86-gcc.bin
 	@mkdir -p $(@D)
 	ret=0; timeout $(TIMEOUT) ./$< > $@ || { ret=$$?; }; echo $$ret >> $@
 
-$(OUTDIR)/%.gcc.out: $(BINDIR)/%.gcc.bin $(SIMUPATH)
+$(OUTDIR)/%.gcc.simu.out: $(BINDIR)/%.gcc.bin $(SIMUPATH)
 	@mkdir -p $(@D)
 	ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@
 
-$(OUTDIR)/%.ccomp.out: $(BINDIR)/%.ccomp.bin $(SIMUPATH)
+$(OUTDIR)/%.ccomp.simu.out: $(BINDIR)/%.ccomp.bin $(SIMUPATH)
 	@mkdir -p $(@D)
 	ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@
 
+$(OUTDIR)/%.gcc.hard.out: $(BINDIR)/%.gcc.bin $(SIMUPATH)
+	@mkdir -p $(@D)
+	ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@
+
+$(OUTDIR)/%.ccomp.hard.out: $(BINDIR)/%.ccomp.bin $(SIMUPATH)
+	@mkdir -p $(@D)
+	ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@
+
 # Assembly to binary
 
 $(BINDIR)/%.x86-gcc.bin: $(ASMDIR)/%.x86-gcc.s $(LIB) $(CCPATH)
diff --git a/test/mppa/interop/Makefile b/test/mppa/interop/Makefile
index e615e89a..3a83d51c 100644
--- a/test/mppa/interop/Makefile
+++ b/test/mppa/interop/Makefile
@@ -6,6 +6,7 @@ CCOMP ?= ccomp
 CFLAGS ?= -O2 -Wno-varargs
 SIMU ?= k1-mppa
 TIMEOUT ?= --signal=SIGTERM 120s
+HARDRUN ?= k1-jtag-runner
 
 DIR=./
 SRCDIR=$(DIR)
@@ -33,17 +34,23 @@ SIMUPATH=$(shell which $(SIMU))
 TESTNAMES ?= $(filter-out $(VAARG_COMMON),$(filter-out $(COMMON),$(notdir $(subst .c,,$(wildcard $(DIR)/*.c)))))
 
 X86_GCC_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .x86-gcc.out,$(TESTNAMES)))
-GCC_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.out,$(TESTNAMES)))
-GCC_REV_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.rev.out,$(TESTNAMES)))
-CCOMP_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.out,$(TESTNAMES)))
+GCC_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.simu.out,$(TESTNAMES)))
+GCC_REV_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.rev.simu.out,$(TESTNAMES)))
+CCOMP_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.simu.out,$(TESTNAMES)))
+
+GCC_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.hard.out,$(TESTNAMES)))
+GCC_REV_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.rev.hard.out,$(TESTNAMES)))
+CCOMP_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.hard.out,$(TESTNAMES)))
 
 VAARG_X86_GCC_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .x86-gcc.vaarg.out,$(TESTNAMES)))
-VAARG_GCC_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.vaarg.out,$(TESTNAMES)))
-VAARG_GCC_REV_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.rev.vaarg.out,$(TESTNAMES)))
-VAARG_CCOMP_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.vaarg.out,$(TESTNAMES)))
+VAARG_GCC_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.vaarg.simu.out,$(TESTNAMES)))
+VAARG_GCC_REV_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.rev.vaarg.simu.out,$(TESTNAMES)))
+VAARG_CCOMP_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.vaarg.simu.out,$(TESTNAMES)))
+
+VAARG_GCC_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.vaarg.hard.out,$(TESTNAMES)))
+VAARG_GCC_REV_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.rev.vaarg.hard.out,$(TESTNAMES)))
+VAARG_CCOMP_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.vaarg.hard.out,$(TESTNAMES)))
 
-OUT=$(X86_GCC_OUT) $(GCC_OUT) $(CCOMP_OUT) $(GCC_REV_OUT)\
-		$(VAARG_GCC_OUT) $(VAARG_GCC_OUT) $(VAARG_CCOMP_OUT) $(VAARG_GCC_REV_OUT)
 BIN=$(addprefix $(BINDIR)/,$(addsuffix .x86-gcc.bin,$(TESTNAMES)))\
 	$(addprefix $(BINDIR)/,$(addsuffix .gcc.bin,$(TESTNAMES)))\
 	$(addprefix $(BINDIR)/,$(addsuffix .ccomp.bin,$(TESTNAMES)))\
@@ -63,14 +70,72 @@ GREEN=\033[0;32m
 RED=\033[0;31m
 NC=\033[0m
 
+.PHONY:
+test: simutest
+
+.PHONY:
+simutest: $(X86_GCC_OUT) $(GCC_SIMUOUT) $(VAARG_X86_GCC_OUT) $(VAARG_GCC_SIMUOUT)
+	@echo "Comparing x86 gcc output to k1 gcc.."
+	@for test in $(TESTNAMES); do\
+		x86out=$(OUTDIR)/$$test.x86-gcc.out;\
+		gccout=$(OUTDIR)/$$test.gcc.simu.out;\
+		vaarg_x86out=$(OUTDIR)/$$test.x86-gcc.vaarg.out;\
+		vaarg_gccout=$(OUTDIR)/$$test.gcc.vaarg.simu.out;\
+		if ! diff $$x86out $$gccout > /dev/null; then\
+			>&2 printf "$(RED)ERROR: $$x86out and $$gccout differ$(NC)\n";\
+		else\
+			printf "$(GREEN)GOOD: $$x86out and $$gccout concur$(NC)\n";\
+		fi;\
+		if ! diff $$vaarg_x86out $$vaarg_gccout > /dev/null; then\
+			>&2 printf "$(RED)ERROR: $$vaarg_x86out and $$vaarg_gccout differ$(NC)\n";\
+		else\
+			printf "$(GREEN)GOOD: $$vaarg_x86out and $$vaarg_gccout concur$(NC)\n";\
+		fi;\
+	done
+
+.PHONY:
+check: simucheck
+
+.PHONY:
+simucheck: $(GCC_SIMUOUT) $(CCOMP_SIMUOUT) $(GCC_REV_SIMUOUT) $(VAARG_GCC_SIMUOUT) $(VAARG_CCOMP_SIMUOUT) $(VAARG_GCC_REV_SIMUOUT)
+	@echo "Comparing k1 gcc output to ccomp.."
+	@for test in $(TESTNAMES); do\
+		gccout=$(OUTDIR)/$$test.gcc.simu.out;\
+		ccompout=$(OUTDIR)/$$test.ccomp.simu.out;\
+		gccrevout=$(OUTDIR)/$$test.gcc.rev.simu.out;\
+		vaarg_gccout=$(OUTDIR)/$$test.gcc.vaarg.simu.out;\
+		vaarg_ccompout=$(OUTDIR)/$$test.ccomp.vaarg.simu.out;\
+		vaarg_gccrevout=$(OUTDIR)/$$test.gcc.rev.vaarg.simu.out;\
+		if ! diff $$ccompout $$gccout > /dev/null; then\
+			>&2 printf "$(RED)ERROR: $$ccompout and $$gccout differ$(NC)\n";\
+		else\
+			printf "$(GREEN)GOOD: $$ccompout and $$gccout concur$(NC)\n";\
+		fi;\
+		if ! diff $$gccrevout $$gccout > /dev/null; then\
+			>&2 printf "$(RED)ERROR: $$gccrevout and $$gccout differ$(NC)\n";\
+		else\
+			printf "$(GREEN)GOOD: $$gccrevout and $$gccout concur$(NC)\n";\
+		fi;\
+		if ! diff $$vaarg_ccompout $$vaarg_gccout > /dev/null; then\
+			>&2 printf "$(RED)ERROR: $$vaarg_ccompout and $$vaarg_gccout differ$(NC)\n";\
+		else\
+			printf "$(GREEN)GOOD: $$vaarg_ccompout and $$vaarg_gccout concur$(NC)\n";\
+		fi;\
+		if ! diff $$vaarg_gccrevout $$vaarg_gccout > /dev/null; then\
+			>&2 printf "$(RED)ERROR: $$vaarg_gccrevout and $$vaarg_gccout differ$(NC)\n";\
+		else\
+			printf "$(GREEN)GOOD: $$vaarg_gccrevout and $$vaarg_gccout concur$(NC)\n";\
+		fi;\
+	done
+
 .PHONY: 
-test: $(X86_GCC_OUT) $(GCC_OUT) $(VAARG_X86_GCC_OUT) $(VAARG_GCC_OUT)
+hardtest: $(X86_GCC_OUT) $(GCC_HARDOUT) $(VAARG_X86_GCC_OUT) $(VAARG_GCC_HARDOUT)
 	@echo "Comparing x86 gcc output to k1 gcc.."
 	@for test in $(TESTNAMES); do\
 		x86out=$(OUTDIR)/$$test.x86-gcc.out;\
-		gccout=$(OUTDIR)/$$test.gcc.out;\
+		gccout=$(OUTDIR)/$$test.gcc.hard.out;\
 		vaarg_x86out=$(OUTDIR)/$$test.x86-gcc.vaarg.out;\
-		vaarg_gccout=$(OUTDIR)/$$test.gcc.vaarg.out;\
+		vaarg_gccout=$(OUTDIR)/$$test.gcc.vaarg.hard.out;\
 		if ! diff $$x86out $$gccout > /dev/null; then\
 			>&2 printf "$(RED)ERROR: $$x86out and $$gccout differ$(NC)\n";\
 		else\
@@ -84,15 +149,15 @@ test: $(X86_GCC_OUT) $(GCC_OUT) $(VAARG_X86_GCC_OUT) $(VAARG_GCC_OUT)
 	done
 
 .PHONY:
-check: $(GCC_OUT) $(CCOMP_OUT) $(GCC_REV_OUT) $(VAARG_GCC_OUT) $(VAARG_CCOMP_OUT) $(VAARG_GCC_REV_OUT)
+hardcheck: $(GCC_HARDOUT) $(CCOMP_HARDOUT) $(GCC_REV_HARDOUT) $(VAARG_GCC_HARDOUT) $(VAARG_CCOMP_HARDOUT) $(VAARG_GCC_REV_HARDOUT)
 	@echo "Comparing k1 gcc output to ccomp.."
 	@for test in $(TESTNAMES); do\
-		gccout=$(OUTDIR)/$$test.gcc.out;\
-		ccompout=$(OUTDIR)/$$test.ccomp.out;\
-		gccrevout=$(OUTDIR)/$$test.gcc.rev.out;\
-		vaarg_gccout=$(OUTDIR)/$$test.gcc.vaarg.out;\
-		vaarg_ccompout=$(OUTDIR)/$$test.ccomp.vaarg.out;\
-		vaarg_gccrevout=$(OUTDIR)/$$test.gcc.rev.vaarg.out;\
+		gccout=$(OUTDIR)/$$test.gcc.hard.out;\
+		ccompout=$(OUTDIR)/$$test.ccomp.hard.out;\
+		gccrevout=$(OUTDIR)/$$test.gcc.rev.hard.out;\
+		vaarg_gccout=$(OUTDIR)/$$test.gcc.vaarg.hard.out;\
+		vaarg_ccompout=$(OUTDIR)/$$test.ccomp.vaarg.hard.out;\
+		vaarg_gccrevout=$(OUTDIR)/$$test.gcc.rev.vaarg.hard.out;\
 		if ! diff $$ccompout $$gccout > /dev/null; then\
 			>&2 printf "$(RED)ERROR: $$ccompout and $$gccout differ$(NC)\n";\
 		else\
@@ -144,36 +209,60 @@ $(OUTDIR)/%.x86-gcc.out: $(BINDIR)/%.x86-gcc.bin
 	@mkdir -p $(@D)
 	ret=0; timeout $(TIMEOUT) ./$< > $@ || { ret=$$?; }; echo $$ret >> $@
 
-$(OUTDIR)/%.gcc.out: $(BINDIR)/%.gcc.bin $(SIMUPATH)
+$(OUTDIR)/%.gcc.simu.out: $(BINDIR)/%.gcc.bin $(SIMUPATH)
 	@mkdir -p $(@D)
 	ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@
 
-$(OUTDIR)/%.gcc.rev.out: $(BINDIR)/%.gcc.rev.bin $(SIMUPATH)
+$(OUTDIR)/%.gcc.rev.simu.out: $(BINDIR)/%.gcc.rev.bin $(SIMUPATH)
 	@mkdir -p $(@D)
 	ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@
 
-$(OUTDIR)/%.ccomp.out: $(BINDIR)/%.ccomp.bin $(SIMUPATH)
+$(OUTDIR)/%.ccomp.simu.out: $(BINDIR)/%.ccomp.bin $(SIMUPATH)
 	@mkdir -p $(@D)
 	ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@
 
+$(OUTDIR)/%.gcc.hard.out: $(BINDIR)/%.gcc.bin $(SIMUPATH)
+	@mkdir -p $(@D)
+	ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@
+
+$(OUTDIR)/%.gcc.rev.hard.out: $(BINDIR)/%.gcc.rev.bin $(SIMUPATH)
+	@mkdir -p $(@D)
+	ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@
+
+$(OUTDIR)/%.ccomp.hard.out: $(BINDIR)/%.ccomp.bin $(SIMUPATH)
+	@mkdir -p $(@D)
+	ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@
+
 ## With vaarg
 
 $(OUTDIR)/%.x86-gcc.vaarg.out: $(BINDIR)/%.x86-gcc.vaarg.bin
 	@mkdir -p $(@D)
 	ret=0; timeout $(TIMEOUT) ./$< > $@ || { ret=$$?; }; echo $$ret >> $@
 
-$(OUTDIR)/%.gcc.vaarg.out: $(BINDIR)/%.gcc.vaarg.bin $(SIMUPATH)
+$(OUTDIR)/%.gcc.vaarg.simu.out: $(BINDIR)/%.gcc.vaarg.bin $(SIMUPATH)
 	@mkdir -p $(@D)
 	ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@
 
-$(OUTDIR)/%.gcc.rev.vaarg.out: $(BINDIR)/%.gcc.rev.vaarg.bin $(SIMUPATH)
+$(OUTDIR)/%.gcc.rev.vaarg.simu.out: $(BINDIR)/%.gcc.rev.vaarg.bin $(SIMUPATH)
 	@mkdir -p $(@D)
 	ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@
 
-$(OUTDIR)/%.ccomp.vaarg.out: $(BINDIR)/%.ccomp.vaarg.bin $(SIMUPATH)
+$(OUTDIR)/%.ccomp.vaarg.simu.out: $(BINDIR)/%.ccomp.vaarg.bin $(SIMUPATH)
 	@mkdir -p $(@D)
 	ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@
 
+$(OUTDIR)/%.gcc.vaarg.hard.out: $(BINDIR)/%.gcc.vaarg.bin $(SIMUPATH)
+	@mkdir -p $(@D)
+	ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@
+
+$(OUTDIR)/%.gcc.rev.vaarg.hard.out: $(BINDIR)/%.gcc.rev.vaarg.bin $(SIMUPATH)
+	@mkdir -p $(@D)
+	ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@
+
+$(OUTDIR)/%.ccomp.vaarg.hard.out: $(BINDIR)/%.ccomp.vaarg.bin $(SIMUPATH)
+	@mkdir -p $(@D)
+	ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@
+
 ##
 # Object to binary
 ##
diff --git a/test/mppa/simucheck.sh b/test/mppa/simucheck.sh
new file mode 100755
index 00000000..25fb9947
--- /dev/null
+++ b/test/mppa/simucheck.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+# Tests the execution of the binaries produced by CompCert, by simulation
+
+source do_test.sh
+
+do_test check $1
diff --git a/test/mppa/test.sh b/test/mppa/simutest.sh
index 30806a6b..3b1021e6 100755
--- a/test/mppa/test.sh
+++ b/test/mppa/simutest.sh
@@ -1,5 +1,5 @@
 #!/bin/bash
-# Tests the validity of the tests
+# Tests the validity of the tests, in simulator
 
 source do_test.sh