Merge branch 'mppa_asmbloc_nobreg' into mppa_k1c

Conflicts:
	mppa_k1c/Asm.v
	mppa_k1c/Asmexpand.ml
	mppa_k1c/TargetPrinter.ml
	test/mppa/Makefile
	test/mppa/builtins/clzll.c
	test/mppa/generate.sh

84 files changed, 499 insertions, 353 deletions

diff --git a/test/mppa/.gitignore b/test/mppa/.gitignore
index f03fc12c..e8ebeff8 100644
--- a/test/mppa/.gitignore
+++ b/test/mppa/.gitignore
@@ -1 +1,20 @@
 check
+asm_coverage
+instr/Makefile
+mmult/Makefile
+prng/Makefile
+sort/Makefile
+prng/.zero
+sort/.zero
+sort/insertion-ccomp-k1c
+sort/insertion-gcc-k1c
+sort/insertion-gcc-x86
+sort/main-ccomp-k1c
+sort/main-gcc-k1c
+sort/main-gcc-x86
+sort/merge-ccomp-k1c
+sort/merge-gcc-k1c
+sort/merge-gcc-x86
+sort/selection-ccomp-k1c
+sort/selection-gcc-k1c
+sort/selection-gcc-x86
diff --git a/test/mppa/Makefile b/test/mppa/Makefile
deleted file mode 100644
index 22f22945..00000000
--- a/test/mppa/Makefile
+++ /dev/null
@@ -1,90 +0,0 @@
-DIR=general
-BINDIR=bin
-ASMDIR=asm
-TESTNAMES=$(notdir $(subst .c,,$(wildcard $(DIR)/*.c)))
-
-CCOMP=../../ccomp
-ELF=$(addprefix $(DIR)/$(BINDIR)/,$(addsuffix .bin,$(TESTNAMES)))
-TOK=$(addprefix $(DIR)/$(BINDIR)/,$(addsuffix .tok,$(TESTNAMES)))
-ASM=$(addprefix $(DIR)/$(ASMDIR)/,$(addsuffix .s,$(TESTNAMES)))
-DEBUG:=$(if $(DEBUG),"-dall",)
-
-.PHONY: all
-all: $(ELF)
-
-nobin: $(ASM)
-
-##
-# Assembling CompCert's assembly file
-##
-$(DIR)/$(BINDIR)/%.bin: $(DIR)/$(ASMDIR)/%.s
-	@mkdir -p $(@D)
-	ccomp $< -o $@
-
-##
-# Compiling the C file with CompCert
-##
-.SECONDARY:
-$(DIR)/$(ASMDIR)/%.s: $(DIR)/%.c $(CCOMP)
-	@mkdir -p $(@D)
-	ccomp $(DEBUG) -O0 -v -S $< -o $@
-
-##
-# A token (.tok) is created if the .bin (created by CompCert) yields the same
-# result as the .bin.exp (created by executing the binary compiled with gcc)
-##
-$(DIR)/$(BINDIR)/%.tok: $(DIR)/$(BINDIR)/%.bin $(DIR)/output/%.bin.exp
-	@mkdir -p $(@D)
-	@bash check.sh $< $@
-
-##
-# Generate .bin.exp : compile with gcc, execute, store the result in .bin.exp
-##
-$(DIR)/output/%.bin.exp: $(DIR)/%.c
-	@bash generate.sh $< $@
-
-.PHONY: FORCE
-FORCE:
-
-.PHONY: check
-check: $(TOK) sort mmult
-
-##
-# A utility displaying which of the pseudo-instructions are covered in the tests
-##
-.PHONY: coverage
-coverage: $(ASM)
-	bash coverage.sh $(DIR)/$(ASMDIR)
-
-##
-# Different versions of a sorting algorithm
-##
-.PHONY: sort
-sort: FORCE
-	(cd sort && make compc-check)
-
-##
-# Different versions of a matrix multiply
-##
-.PHONY: mmult
-mmult: FORCE
-	(cd mmult && make compc-check)
-
-.PHONY: clean
-clean:
-	rm -f $(DIR)/*.alloctrace
-	rm -f $(DIR)/*.cm
-	rm -f $(DIR)/*.compcert.c
-	rm -f $(DIR)/*.i
-	rm -f $(DIR)/*.light.c
-	rm -f $(DIR)/*.ltl
-	rm -f $(DIR)/*.mach
-	rm -f $(DIR)/*.parsed.c
-	rm -f $(DIR)/*.rtl.?
-	rm -f $(DIR)/$(ASMDIR)/*.s
-	rm -f $(DIR)/$(BINDIR)/*.bin
-	rm -f $(DIR)/$(BINDIR)/*.tok
-	rm -f $(DIR)/output/*.out
-	rm -f $(DIR)/output/*.exp
-	rm -rf $(DIR)/profile/
-	rm -f $(ELF)
diff --git a/test/mppa/builtins/clzll.c b/test/mppa/builtins/clzll.c
new file mode 100644
index 00000000..13905cba
--- /dev/null
+++ b/test/mppa/builtins/clzll.c
@@ -0,0 +1,7 @@
+#include "framework.h"
+
+BEGIN_TEST(long long)
+{
+    c = __builtin_clzll(a);
+}
+END_TEST()
diff --git a/test/mppa/general/stsud.c b/test/mppa/builtins/stsud.c
index fb07b94f..fb07b94f 100644
--- a/test/mppa/general/stsud.c
+++ b/test/mppa/builtins/stsud.c
diff --git a/test/mppa/check.sh b/test/mppa/check.sh
index dd9691be..8db50f1b 100644..100755
--- a/test/mppa/check.sh
+++ b/test/mppa/check.sh
@@ -1,32 +1,6 @@
-# $1: binary file to check
-# $2: output check token
+#!/bin/bash
+# Tests the execution of the binaries produced by CompCert
 
-elffile="$1"
-token="$2"
+source do_test.sh
 
-if [ ! -f $elffile ]; then
-	>&2 echo "ERROR: $elffile not found"
-	shift; continue
-fi
-
-dir="$(dirname $elffile)"
-elf="$(basename $elffile)"
-
-exp="$dir/../output/$elf.exp"
-out="$dir/../output/$elf.out"
-if [ ! -f $exp ]; then
-	>&2 echo "ERROR: $exp not found"
-	exit
-fi
-
-k1-cluster -- $elffile > $out
-echo $? >> $out
-
-if ! diff $exp $out; then
-	>&2 echo "ERROR: $exp and $out differ"
-	exit
-fi
-
-echo "PASSED: $elf"
-touch $token
-#shift
+do_test check
diff --git a/test/mppa/do_test.sh b/test/mppa/do_test.sh
new file mode 100644
index 00000000..ee7cbcf7
--- /dev/null
+++ b/test/mppa/do_test.sh
@@ -0,0 +1,33 @@
+do_test () {
+cat << EOF
+
+##
+# PRNG tests
+##
+EOF
+(cd prng && make $1 -j8)
+
+cat << EOF
+
+##
+# Matrix Multiplication tests
+##
+EOF
+(cd mmult && make $1 -j8)
+
+cat << EOF
+
+##
+# List sort tests
+##
+EOF
+(cd sort && make $1 -j8)
+
+cat << EOF
+
+##
+# Instruction unit tests
+##
+EOF
+(cd instr && make $1 -j8)
+}
diff --git a/test/mppa/generate.sh b/test/mppa/generate.sh
deleted file mode 100644
index ea633724..00000000
--- a/test/mppa/generate.sh
+++ /dev/null
@@ -1,21 +0,0 @@
-# $1: c file to examine
-# $2: write file
-
-cfile="$1"
-writefile="$2"
-
-dirwritefile=$(dirname $writefile)
-asmdir=$dirwritefile/../asm/gcc
-
-if [ ! -f $cfile ]; then
-	>&2 echo "ERROR: $cfile not found"
-	shift; continue
-fi
-
-mkdir -p $dirwritefile
-mkdir -p $asmdir
-
-tmpbin=/tmp/k1-$(basename $1)-bin 
-k1-gcc -O0 $1 -S -o $asmdir/$(basename $1).s
-k1-gcc -O0 $1 -o $tmpbin
-(k1-cluster -- $tmpbin; echo $? > $2)
diff --git a/test/mppa/general/.gitignore b/test/mppa/instr/.gitignore
index ea1472ec..ea1472ec 100644
--- a/test/mppa/general/.gitignore
+++ b/test/mppa/instr/.gitignore
diff --git a/test/mppa/instr/Makefile b/test/mppa/instr/Makefile
new file mode 100644
index 00000000..89ff9a73
--- /dev/null
+++ b/test/mppa/instr/Makefile
@@ -0,0 +1,111 @@
+K1CC ?= k1-mbr-gcc
+CC ?= gcc
+CCOMP ?= ccomp
+CFLAGS ?= -O2
+SIMU ?= k1-cluster
+TIMEOUT ?= 10s
+
+DIR=./
+SRCDIR=$(DIR)
+OUTDIR=$(DIR)/out
+BINDIR=$(DIR)/bin
+ASMDIR=$(DIR)/asm
+
+##
+# Intended flow : .c -> .gcc.s -> .gcc.bin -> .gcc.out
+#                    -> .ccomp.s -> .ccomp.bin -> .ccomp.out
+##
+
+K1CCPATH=$(shell which $(K1CC))
+CCPATH=$(shell which $(CC))
+CCOMPPATH=$(shell which $(CCOMP))
+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)))
+
+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)))
+
+##
+# Targets
+##
+
+all: $(BIN)
+
+.PHONY:
+test: $(X86_GCC_OUT) $(GCC_OUT)
+	@echo "Comparing x86 gcc output to k1 gcc.."
+	@for test in $(TESTNAMES); do\
+		x86out=$(OUTDIR)/$$test.x86-gcc.out;\
+		gccout=$(OUTDIR)/$$test.gcc.out;\
+		if ! diff $$x86out $$gccout; then\
+			>&2 echo "ERROR: $$x86out and $$gccout differ";\
+		else\
+			echo "GOOD: $$x86out and $$gccout concur";\
+		fi;\
+	done
+
+.PHONY:
+check: $(GCC_OUT) $(CCOMP_OUT)
+	@echo "Comparing k1 gcc output to ccomp.."
+	@for test in $(TESTNAMES); do\
+		gccout=$(OUTDIR)/$$test.gcc.out;\
+		ccompout=$(OUTDIR)/$$test.ccomp.out;\
+		if ! diff $$ccompout $$gccout; then\
+			>&2 echo "ERROR: $$ccompout and $$gccout differ";\
+		else\
+			echo "GOOD: $$ccompout and $$gccout concur";\
+		fi;\
+	done
+
+##
+# Rules
+##
+
+.SECONDARY:
+# Generating output
+
+$(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)
+	@mkdir -p $(@D)
+	ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@
+
+$(OUTDIR)/%.ccomp.out: $(BINDIR)/%.ccomp.bin $(SIMUPATH)
+	@mkdir -p $(@D)
+	ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@
+
+# Assembly to binary
+
+$(BINDIR)/%.x86-gcc.bin: $(ASMDIR)/%.x86-gcc.s $(CCPATH)
+	@mkdir -p $(@D)
+	$(CC) $(CFLAGS) $< -o $@
+
+$(BINDIR)/%.gcc.bin: $(ASMDIR)/%.gcc.s $(K1CCPATH)
+	@mkdir -p $(@D)
+	$(K1CC) $(CFLAGS) $< -o $@
+
+$(BINDIR)/%.ccomp.bin: $(ASMDIR)/%.ccomp.s $(CCOMPPATH)
+	@mkdir -p $(@D)
+	$(CCOMP) $(CFLAGS) $< -o $@
+
+# Source to assembly
+
+$(ASMDIR)/%.x86-gcc.s: $(SRCDIR)/%.c $(CCPATH)
+	@mkdir -p $(@D)
+	$(CC) $(CFLAGS) -S $< -o $@
+
+$(ASMDIR)/%.gcc.s: $(SRCDIR)/%.c $(K1CCPATH)
+	@mkdir -p $(@D)
+	$(K1CC) $(CFLAGS) -S $< -o $@
+
+$(ASMDIR)/%.ccomp.s: $(SRCDIR)/%.c $(CCOMPPATH)
+	@mkdir -p $(@D)
+	$(CCOMP) $(CFLAGS) -S $< -o $@
diff --git a/test/mppa/general/addw.c b/test/mppa/instr/addw.c
index be8afc67..be8afc67 100644
--- a/test/mppa/general/addw.c
+++ b/test/mppa/instr/addw.c
diff --git a/test/mppa/general/andd.c b/test/mppa/instr/andd.c
index 4f503764..4f503764 100644
--- a/test/mppa/general/andd.c
+++ b/test/mppa/instr/andd.c
diff --git a/test/mppa/general/andw.c b/test/mppa/instr/andw.c
index 99de0049..99de0049 100644
--- a/test/mppa/general/andw.c
+++ b/test/mppa/instr/andw.c
diff --git a/test/mppa/general/branch.c b/test/mppa/instr/branch.c
index 72e7e20e..72e7e20e 100644
--- a/test/mppa/general/branch.c
+++ b/test/mppa/instr/branch.c
diff --git a/test/mppa/general/branchz.c b/test/mppa/instr/branchz.c
index fb86d357..fb86d357 100644
--- a/test/mppa/general/branchz.c
+++ b/test/mppa/instr/branchz.c
diff --git a/test/mppa/general/branchzu.c b/test/mppa/instr/branchzu.c
index 97adb605..97adb605 100644
--- a/test/mppa/general/branchzu.c
+++ b/test/mppa/instr/branchzu.c
diff --git a/test/mppa/general/call.c b/test/mppa/instr/call.c
index 727cef63..727cef63 100644
--- a/test/mppa/general/call.c
+++ b/test/mppa/instr/call.c
diff --git a/test/mppa/general/cb.deqz.c b/test/mppa/instr/cb.deqz.c
index c56733f0..c56733f0 100644
--- a/test/mppa/general/cb.deqz.c
+++ b/test/mppa/instr/cb.deqz.c
diff --git a/test/mppa/general/cb.dgez.c b/test/mppa/instr/cb.dgez.c
index abb6ec57..abb6ec57 100644
--- a/test/mppa/general/cb.dgez.c
+++ b/test/mppa/instr/cb.dgez.c
diff --git a/test/mppa/general/cb.dgtz.c b/test/mppa/instr/cb.dgtz.c
index d4271845..d4271845 100644
--- a/test/mppa/general/cb.dgtz.c
+++ b/test/mppa/instr/cb.dgtz.c
diff --git a/test/mppa/general/cb.dlez.c b/test/mppa/instr/cb.dlez.c
index 18e67f06..18e67f06 100644
--- a/test/mppa/general/cb.dlez.c
+++ b/test/mppa/instr/cb.dlez.c
diff --git a/test/mppa/general/cb.dltz.c b/test/mppa/instr/cb.dltz.c
index 366aea49..366aea49 100644
--- a/test/mppa/general/cb.dltz.c
+++ b/test/mppa/instr/cb.dltz.c
diff --git a/test/mppa/general/cb.dnez.c b/test/mppa/instr/cb.dnez.c
index 81c2cd29..81c2cd29 100644
--- a/test/mppa/general/cb.dnez.c
+++ b/test/mppa/instr/cb.dnez.c
diff --git a/test/mppa/general/cb.wgez.c b/test/mppa/instr/cb.wgez.c
index 477f4bc6..477f4bc6 100644
--- a/test/mppa/general/cb.wgez.c
+++ b/test/mppa/instr/cb.wgez.c
diff --git a/test/mppa/general/cb.wgtz.c b/test/mppa/instr/cb.wgtz.c
index c9ab9a06..c9ab9a06 100644
--- a/test/mppa/general/cb.wgtz.c
+++ b/test/mppa/instr/cb.wgtz.c
diff --git a/test/mppa/general/cb.wlez.c b/test/mppa/instr/cb.wlez.c
index c3069fda..c3069fda 100644
--- a/test/mppa/general/cb.wlez.c
+++ b/test/mppa/instr/cb.wlez.c
diff --git a/test/mppa/general/cb.wltz.c b/test/mppa/instr/cb.wltz.c
index 6cf5fcf0..6cf5fcf0 100644
--- a/test/mppa/general/cb.wltz.c
+++ b/test/mppa/instr/cb.wltz.c
diff --git a/test/mppa/general/compd.eq.c b/test/mppa/instr/compd.eq.c
index d19a4d20..d19a4d20 100644
--- a/test/mppa/general/compd.eq.c
+++ b/test/mppa/instr/compd.eq.c
diff --git a/test/mppa/general/compd.geu.c b/test/mppa/instr/compd.geu.c
index edc31183..edc31183 100644
--- a/test/mppa/general/compd.geu.c
+++ b/test/mppa/instr/compd.geu.c
diff --git a/test/mppa/general/compd.gt.c b/test/mppa/instr/compd.gt.c
index 24147779..24147779 100644
--- a/test/mppa/general/compd.gt.c
+++ b/test/mppa/instr/compd.gt.c
diff --git a/test/mppa/general/compd.gtu.c b/test/mppa/instr/compd.gtu.c
index 5ce82569..5ce82569 100644
--- a/test/mppa/general/compd.gtu.c
+++ b/test/mppa/instr/compd.gtu.c
diff --git a/test/mppa/general/compd.le.c b/test/mppa/instr/compd.le.c
index a84aad97..a84aad97 100644
--- a/test/mppa/general/compd.le.c
+++ b/test/mppa/instr/compd.le.c
diff --git a/test/mppa/general/compd.leu.c b/test/mppa/instr/compd.leu.c
index e386bc27..e386bc27 100644
--- a/test/mppa/general/compd.leu.c
+++ b/test/mppa/instr/compd.leu.c
diff --git a/test/mppa/general/compd.lt.c b/test/mppa/instr/compd.lt.c
index df07a708..df07a708 100644
--- a/test/mppa/general/compd.lt.c
+++ b/test/mppa/instr/compd.lt.c
diff --git a/test/mppa/general/compd.ltu.c b/test/mppa/instr/compd.ltu.c
index dfaa8921..dfaa8921 100644
--- a/test/mppa/general/compd.ltu.c
+++ b/test/mppa/instr/compd.ltu.c
diff --git a/test/mppa/general/compd.ne.c b/test/mppa/instr/compd.ne.c
index 19ce0a69..19ce0a69 100644
--- a/test/mppa/general/compd.ne.c
+++ b/test/mppa/instr/compd.ne.c
diff --git a/test/mppa/general/compw.eq.c b/test/mppa/instr/compw.eq.c
index dc7a3ab1..dc7a3ab1 100644
--- a/test/mppa/general/compw.eq.c
+++ b/test/mppa/instr/compw.eq.c
diff --git a/test/mppa/general/compw.geu.c b/test/mppa/instr/compw.geu.c
index d72ca56c..d72ca56c 100644
--- a/test/mppa/general/compw.geu.c
+++ b/test/mppa/instr/compw.geu.c
diff --git a/test/mppa/general/compw.gt.c b/test/mppa/instr/compw.gt.c
index 9ad02610..9ad02610 100644
--- a/test/mppa/general/compw.gt.c
+++ b/test/mppa/instr/compw.gt.c
diff --git a/test/mppa/general/compw.gtu.c b/test/mppa/instr/compw.gtu.c
index 77f04989..77f04989 100644
--- a/test/mppa/general/compw.gtu.c
+++ b/test/mppa/instr/compw.gtu.c
diff --git a/test/mppa/general/compw.le.c b/test/mppa/instr/compw.le.c
index b7a7a432..b7a7a432 100644
--- a/test/mppa/general/compw.le.c
+++ b/test/mppa/instr/compw.le.c
diff --git a/test/mppa/general/compw.leu.c b/test/mppa/instr/compw.leu.c
index 4892f06c..4892f06c 100644
--- a/test/mppa/general/compw.leu.c
+++ b/test/mppa/instr/compw.leu.c
diff --git a/test/mppa/general/compw.lt.c b/test/mppa/instr/compw.lt.c
index 2cc151bf..2cc151bf 100644
--- a/test/mppa/general/compw.lt.c
+++ b/test/mppa/instr/compw.lt.c
diff --git a/test/mppa/general/compw.ltu.c b/test/mppa/instr/compw.ltu.c
index b524127f..b524127f 100644
--- a/test/mppa/general/compw.ltu.c
+++ b/test/mppa/instr/compw.ltu.c
diff --git a/test/mppa/general/compw.ne.c b/test/mppa/instr/compw.ne.c
index 433b0b86..433b0b86 100644
--- a/test/mppa/general/compw.ne.c
+++ b/test/mppa/instr/compw.ne.c
diff --git a/test/mppa/general/div2.c b/test/mppa/instr/div2.c
index 01a4b575..01a4b575 100644
--- a/test/mppa/general/div2.c
+++ b/test/mppa/instr/div2.c
diff --git a/test/mppa/general/for.c b/test/mppa/instr/for.c
index d6870afb..d6870afb 100644
--- a/test/mppa/general/for.c
+++ b/test/mppa/instr/for.c
diff --git a/test/mppa/general/forvar.c b/test/mppa/instr/forvar.c
index 57548274..57548274 100644
--- a/test/mppa/general/forvar.c
+++ b/test/mppa/instr/forvar.c
diff --git a/test/mppa/general/forvarl.c b/test/mppa/instr/forvarl.c
index 30717a51..30717a51 100644
--- a/test/mppa/general/forvarl.c
+++ b/test/mppa/instr/forvarl.c
diff --git a/test/mppa/general/framework.h b/test/mppa/instr/framework.h
index b7dc4933..52ba97bc 100644
--- a/test/mppa/general/framework.h
+++ b/test/mppa/instr/framework.h
@@ -1,7 +1,7 @@
 #ifndef __FRAMEWORK_H__
 #define __FRAMEWORK_H__
 
-#include "../lib/prng.c"
+#include "../prng/prng.c"
 
 #define BEGIN_TEST_N(type, N)\
     int main(void){\
diff --git a/test/mppa/general/lbs.c b/test/mppa/instr/lbs.c
index f104d62b..f104d62b 100644
--- a/test/mppa/general/lbs.c
+++ b/test/mppa/instr/lbs.c
diff --git a/test/mppa/general/lbz.c b/test/mppa/instr/lbz.c
index 2deeaebe..2deeaebe 100644
--- a/test/mppa/general/lbz.c
+++ b/test/mppa/instr/lbz.c
diff --git a/test/mppa/general/muld.c b/test/mppa/instr/muld.c
index 9a40f389..9a40f389 100644
--- a/test/mppa/general/muld.c
+++ b/test/mppa/instr/muld.c
diff --git a/test/mppa/general/mulw.c b/test/mppa/instr/mulw.c
index bf517ce8..bf517ce8 100644
--- a/test/mppa/general/mulw.c
+++ b/test/mppa/instr/mulw.c
diff --git a/test/mppa/general/negd.c b/test/mppa/instr/negd.c
index a8e8ff45..a8e8ff45 100644
--- a/test/mppa/general/negd.c
+++ b/test/mppa/instr/negd.c
diff --git a/test/mppa/general/ord.c b/test/mppa/instr/ord.c
index eaedcb28..eaedcb28 100644
--- a/test/mppa/general/ord.c
+++ b/test/mppa/instr/ord.c
diff --git a/test/mppa/general/sbfd.c b/test/mppa/instr/sbfd.c
index 912f1fdb..912f1fdb 100644
--- a/test/mppa/general/sbfd.c
+++ b/test/mppa/instr/sbfd.c
diff --git a/test/mppa/general/sbfw.c b/test/mppa/instr/sbfw.c
index feffd497..feffd497 100644
--- a/test/mppa/general/sbfw.c
+++ b/test/mppa/instr/sbfw.c
diff --git a/test/mppa/general/simple.c b/test/mppa/instr/simple.c
index 89bba27e..89bba27e 100644
--- a/test/mppa/general/simple.c
+++ b/test/mppa/instr/simple.c
diff --git a/test/mppa/general/sllw.c b/test/mppa/instr/sllw.c
index df55c9e8..df55c9e8 100644
--- a/test/mppa/general/sllw.c
+++ b/test/mppa/instr/sllw.c
diff --git a/test/mppa/general/srad.c b/test/mppa/instr/srad.c
index b4047bc7..b4047bc7 100644
--- a/test/mppa/general/srad.c
+++ b/test/mppa/instr/srad.c
diff --git a/test/mppa/general/srld.c b/test/mppa/instr/srld.c
index 71e82b2a..71e82b2a 100644
--- a/test/mppa/general/srld.c
+++ b/test/mppa/instr/srld.c
diff --git a/test/mppa/general/udivd.c b/test/mppa/instr/udivd.c
index 52e0d412..52e0d412 100644
--- a/test/mppa/general/udivd.c
+++ b/test/mppa/instr/udivd.c
diff --git a/test/mppa/general/umodd.c b/test/mppa/instr/umodd.c
index e7dd506f..e7dd506f 100644
--- a/test/mppa/general/umodd.c
+++ b/test/mppa/instr/umodd.c
diff --git a/test/mppa/general/xord.c b/test/mppa/instr/xord.c
index b9d86f06..b9d86f06 100644
--- a/test/mppa/general/xord.c
+++ b/test/mppa/instr/xord.c
diff --git a/test/mppa/lib/.gitignore b/test/mppa/lib/.gitignore
deleted file mode 100644
index 1879eaee..00000000
--- a/test/mppa/lib/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-prng-test-k1c
-prng-test-x86
diff --git a/test/mppa/lib/Makefile b/test/mppa/lib/Makefile
deleted file mode 100644
index 7aeab9f3..00000000
--- a/test/mppa/lib/Makefile
+++ /dev/null
@@ -1,30 +0,0 @@
-prng-test-x86: prng.c
-	gcc -D__UNIT_TEST_PRNG__ -O2 -std=c99 $< -o $@
-
-prng-test-k1c: prng.c
-	k1-gcc -D__UNIT_TEST_PRNG__ -O2 -std=c99 $< -o $@
-
-.PHONY:
-test: test-x86 test-k1c
-
-.PHONY:
-test-x86: prng-test-x86
-	@if ! ./$<; then\
-		>&2 echo "ERROR: $< failed";\
-		exit;\
-	else\
-		echo "x86: Test Succeeded";\
-	fi
-
-.PHONY:
-test-k1c: prng-test-k1c
-	@if ! k1-cluster -- ./$<; then\
-		>&2 echo "ERROR: $< failed";\
-		exit;\
-	else\
-		echo "k1c: Test Succeeded";\
-	fi
-
-.PHONY:
-clean:
-	rm -f prng-test-x86 prng-test-k1c
diff --git a/test/mppa/mmult/.gitignore b/test/mppa/mmult/.gitignore
index 5883d367..c9cd4c65 100644
--- a/test/mppa/mmult/.gitignore
+++ b/test/mppa/mmult/.gitignore
@@ -1,3 +1,4 @@
-mmult-test-k1c
-mmult-test-x86
-test-ccomp
+mmult-test-ccomp-k1c
+mmult-test-gcc-k1c
+mmult-test-gcc-x86
+.zero
diff --git a/test/mppa/mmult/Makefile b/test/mppa/mmult/Makefile
index 23b31d49..cf82e359 100644
--- a/test/mppa/mmult/Makefile
+++ b/test/mppa/mmult/Makefile
@@ -1,78 +1,67 @@
-PRNG=../lib/prng.c
-CCOMP=../../../ccomp
-
-ALL= mmult-test-x86 mmult-test-k1c\
+K1CC ?= k1-mbr-gcc
+CC ?= gcc
+CCOMP ?= ccomp
+CFLAGS ?= -O2
+SIMU ?= k1-cluster
+TIMEOUT ?= 10s
+
+K1CCPATH=$(shell which $(K1CC))
+CCPATH=$(shell which $(CC))
+CCOMPPATH=$(shell which $(CCOMP))
+SIMUPATH=$(shell which $(SIMU))
+
+PRNG=../prng/prng.c
+
+ALL= mmult-test-gcc-x86 mmult-test-gcc-k1c mmult-test-ccomp-k1c
+CCOMP_OUT= mmult-test-ccomp-k1c.out
+GCC_OUT= mmult-test-gcc-k1c.out
+X86_GCC_OUT= mmult-test-gcc-x86.out
+STUB_OUT=.zero
 
 all: $(ALL)
 
-%-test-x86: %.c $(PRNG)
-	gcc -D__UNIT_TEST_$$(echo $(basename $<) | tr a-z A-Z)__ -O2 -std=c99 $^ -o $@
-
-%-test-k1c: %.c $(PRNG)
-	k1-gcc -D__UNIT_TEST_$$(echo $(basename $<) | tr a-z A-Z)__ -O2 -std=c99 $^ -o $@
+mmult-test-gcc-x86: mmult.c $(PRNG) $(CCPATH)
+	$(CC) $(CFLAGS) $(filter-out $(CCPATH),$^) -o $@
 
-test-x86: mmult.c $(PRNG)
-	gcc -O2 -std=c99 $^ -o $@
+mmult-test-gcc-k1c: mmult.c $(PRNG) $(K1CCPATH)
+	$(K1CC) $(CFLAGS) $(filter-out $(K1CCPATH),$^) -o $@
 
-test-k1c: mmult.c $(PRNG)
-	k1-gcc -O2 -std=c99 $^ -o $@
+mmult-test-ccomp-k1c: mmult.c $(PRNG) $(CCOMPPATH)
+	$(CCOMP) $(CFLAGS) $(filter-out $(CCOMPPATH),$^) -o $@
 
-%.s: %.c $(CCOMP)
-	ccomp -O2 -S $< -o $@
+.SECONDARY:
+%k1c.out: %k1c $(SIMUPATH)
+	ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@
 
-test-ccomp: mmult.s $(subst .c,.s,$(PRNG))
-	k1-gcc $^ -o $@
+%x86.out: %x86
+	ret=0; timeout $(TIMEOUT) ./$< > $@ || { ret=$$?; }; echo $$ret >> $@
 
-.PHONY:
-unittest: unittest-x86 unittest-k1c
+.zero:
+	@echo "0" > $@
 
 .PHONY:
-check: check-x86 check-k1c
+test: test-x86 test-k1c
 
 .PHONY:
-compc-check: test-ccomp
-	@if ! k1-cluster -- ./$<; then\
-		>&2 echo "ERROR k1c: mmult $< failed";\
+test-x86: $(X86_GCC_OUT) $(STUB_OUT)
+	@if ! diff $< $(STUB_OUT); then\
+		>&2 echo "ERROR x86: $< failed";\
 	else\
-		echo "k1c: Test mmult $< succeeded";\
+		echo "GOOD x86: $< succeeded";\
 	fi
 
 .PHONY:
-check-x86: test-x86
-	@if ! ./$<; then\
-		>&2 echo "ERROR x86: $< failed";\
+test-k1c: $(GCC_OUT) $(STUB_OUT)
+	@if ! diff $< $(STUB_OUT); then\
+		>&2 echo "ERROR k1c: $< failed";\
 	else\
-		echo "x86: Test $< succeeded";\
+		echo "GOOD k1c: $< succeeded";\
 	fi
 
 .PHONY:
-check-k1c: test-k1c
-	@if ! k1-cluster -- ./$<; then\
+check: $(CCOMP_OUT) $(STUB_OUT)
+	@if ! diff $< $(STUB_OUT); then\
 		>&2 echo "ERROR k1c: $< failed";\
 	else\
-		echo "k1c: Test $< succeeded";\
+		echo "GOOD k1c: $< succeeded";\
 	fi
-
-.PHONY:
-unittest-x86: mmult-test-x86
-	@for test in $^; do\
-		if ! ./$$test; then\
-			>&2 echo "ERROR x86: $$test failed";\
-		else\
-			echo "x86: Test $$test Succeeded";\
-		fi;\
-	done
-
-.PHONY:
-unittest-k1c: mmult-test-k1c
-	@for test in $^; do\
-		if ! k1-cluster -- ./$$test; then\
-			>&2 echo "ERROR k1c: $$test failed";\
-		else\
-			echo "k1c: Test $$test Succeeded";\
-		fi;\
-	done
-
-.PHONY:
-clean:
-	rm -f $(ALL)
diff --git a/test/mppa/mmult/README.md b/test/mppa/mmult/README.md
new file mode 100644
index 00000000..ef2bff7e
--- /dev/null
+++ b/test/mppa/mmult/README.md
@@ -0,0 +1,17 @@
+MMULT
+=====
+
+Examples of matrix multiplication using different methods.
+
+We compute matrix multiplication using column-based matrix multiplication, then row-based, and finally block based.
+
+The test verifies that the result is the same on the three methods. If it is the same, 0 will be returned.
+
+The following commands can be run inside the folder:
+
+- `make`: produces the unitary test binaries
+  - `mmult-test-gcc-x86` : binary from gcc on x86
+  - `mmult-test-k1c-x86` : binary from gcc on k1c
+  - `mmult-test-ccomp-x86` : binary from ccomp on k1c
+- `make test`: tests the return value of the binaries produced by gcc.
+- `make check`: tests the return value of the binary produced by CompCert.
diff --git a/test/mppa/mmult/mmult.c b/test/mppa/mmult/mmult.c
index b674ca80..aeb91d48 100644
--- a/test/mppa/mmult/mmult.c
+++ b/test/mppa/mmult/mmult.c
@@ -1,5 +1,5 @@
-#include "../lib/types.h"
-#include "../lib/prng.h"
+#include "../prng/types.h"
+#include "../prng/prng.h"
 
 #define __UNIT_TEST_MMULT__
 
@@ -10,24 +10,28 @@
 #endif
 
 void mmult_row(uint64_t C[][SIZE], uint64_t A[][SIZE], uint64_t B[][SIZE]){
-    for (int i = 0 ; i < SIZE ; i++)
-        for (int j = 0 ; j < SIZE ; j++)
+    int i, j, k;
+
+    for (i = 0 ; i < SIZE ; i++)
+        for (j = 0 ; j < SIZE ; j++)
             C[i][j] = 0;
 
-    for (int i = 0 ; i < SIZE ; i++)
-        for (int j = 0 ; j < SIZE ; j++)
-            for (int k = 0 ; k < SIZE ; k++)
+    for (i = 0 ; i < SIZE ; i++)
+        for (j = 0 ; j < SIZE ; j++)
+            for (k = 0 ; k < SIZE ; k++)
                 C[i][j] += A[i][k] * B[k][j];
 }
 
 void mmult_col(uint64_t C[][SIZE], uint64_t A[][SIZE], uint64_t B[][SIZE]){
-    for (int i = 0 ; i < SIZE ; i++)
-        for (int j = 0 ; j < SIZE ; j++)
+    int i, j, k;
+
+    for (i = 0 ; i < SIZE ; i++)
+        for (j = 0 ; j < SIZE ; j++)
             C[i][j] = 0;
 
-    for (int k = 0 ; k < SIZE ; k++)
-        for (int i = 0 ; i < SIZE ; i++)
-            for (int j = 0 ; j < SIZE ; j++)
+    for (k = 0 ; k < SIZE ; k++)
+        for (i = 0 ; i < SIZE ; i++)
+            for (j = 0 ; j < SIZE ; j++)
                 C[i][j] += A[i][k] * B[k][j];
 }
 
@@ -41,10 +45,11 @@ typedef struct mblock {
 
 void divac_mul(mblock *C, const mblock *A, const mblock *B){
     const int size = C->imax - C->imin;
+    int i, j, k;
 
-    for (int i = 0 ; i < size ; i++)
-        for (int j = 0 ; j < size ; j++)
-            for (int k = 0 ; k < size ; k++)
+    for (i = 0 ; i < size ; i++)
+        for (j = 0 ; j < size ; j++)
+            for (k = 0 ; k < size ; k++)
                 MAT_IJ(C, i, j) += MAT_IJ(A, i, k) * MAT_IJ(B, k, j);
 }
 
@@ -119,9 +124,10 @@ static uint64_t A[SIZE][SIZE], B[SIZE][SIZE];
 
 int main(void){
     srand(42);
+    int i, j;
 
-    for (int i = 0 ; i < SIZE ; i++)
-        for (int j = 0 ; j < SIZE ; j++){
+    for (i = 0 ; i < SIZE ; i++)
+        for (j = 0 ; j < SIZE ; j++){
             A[i][j] = randlong();
             B[i][j] = randlong();
         }
@@ -130,8 +136,8 @@ int main(void){
     mmult_col(C2, A, B);
     mmult_divac(C3, A, B);
 
-    for (int i = 0 ; i < SIZE ; i++)
-        for (int j = 0 ; j < SIZE ; j++)
+    for (i = 0 ; i < SIZE ; i++)
+        for (j = 0 ; j < SIZE ; j++)
             if (!(C1[i][j] == C2[i][j] && C1[i][j] == C3[i][j]))
                 return -1;
 
diff --git a/test/mppa/prng/.gitignore b/test/mppa/prng/.gitignore
new file mode 100644
index 00000000..0792a78b
--- /dev/null
+++ b/test/mppa/prng/.gitignore
@@ -0,0 +1,3 @@
+prng-test-ccomp-k1c
+prng-test-gcc-x86
+prng-test-gcc-k1c
diff --git a/test/mppa/prng/Makefile b/test/mppa/prng/Makefile
new file mode 100644
index 00000000..5580cd8e
--- /dev/null
+++ b/test/mppa/prng/Makefile
@@ -0,0 +1,69 @@
+K1CC ?= k1-mbr-gcc
+CC ?= gcc
+CCOMP ?= ccomp
+CFLAGS ?= -O2
+SIMU ?= k1-cluster
+TIMEOUT ?= 10s
+
+K1CCPATH=$(shell which $(K1CC))
+CCPATH=$(shell which $(CC))
+CCOMPPATH=$(shell which $(CCOMP))
+SIMUPATH=$(shell which $(SIMU))
+
+ALL= prng-test-gcc-x86 prng-test-gcc-k1c prng-test-ccomp-k1c
+CCOMP_OUT= prng-test-ccomp-k1c.out
+GCC_OUT= prng-test-gcc-k1c.out
+X86_GCC_OUT= prng-test-gcc-x86.out
+STUB_OUT=.zero
+
+all: $(ALL)
+
+prng-test-gcc-x86: prng.c $(CCPATH)
+	$(CC) -D__UNIT_TEST_PRNG__ $(CFLAGS) $< -o $@
+
+prng-test-gcc-k1c: prng.c $(K1CCPATH)
+	$(K1CC) -D__UNIT_TEST_PRNG__ $(CFLAGS) $< -o $@
+
+prng-test-ccomp-k1c: prng.c $(CCOMPPATH)
+	$(CCOMP) -D__UNIT_TEST_PRNG__ $(CFLAGS) $< -o $@
+
+.SECONDARY:
+%k1c.out: %k1c $(SIMUPATH)
+	ret=0; timeout $(TIMEOUT) $(SIMU) -- $<  > $@ || { ret=$$?; }; echo $$ret >> $@
+
+%x86.out: %x86
+	ret=0; timeout $(TIMEOUT) ./$< > $@ || { ret=$$?; }; echo $$ret >> $@
+
+.zero:
+	@echo "0" > $@
+
+.PHONY:
+test: test-x86 test-k1c
+
+.PHONY:
+test-x86: $(X86_GCC_OUT) $(STUB_OUT)
+	@if ! diff $< $(STUB_OUT); then\
+		>&2 echo "ERROR x86: $< failed";\
+	else\
+		echo "GOOD x86: $< succeeded";\
+	fi
+
+.PHONY:
+test-k1c: $(GCC_OUT) $(STUB_OUT)
+	@if ! diff $< $(STUB_OUT); then\
+		>&2 echo "ERROR k1c: $< failed";\
+	else\
+		echo "GOOD k1c: $< succeeded";\
+	fi
+
+.PHONY:
+check: $(CCOMP_OUT) $(STUB_OUT)
+	@if ! diff $< $(STUB_OUT); then\
+		>&2 echo "ERROR k1c: $< failed";\
+	else\
+		echo "GOOD k1c: $< succeeded";\
+	fi
+
+.PHONY:
+clean:
+	rm -f prng-test-gcc-x86 prng-test-gcc-k1c prng-test-ccomp-k1c
diff --git a/test/mppa/prng/README.md b/test/mppa/prng/README.md
new file mode 100644
index 00000000..b4c2279b
--- /dev/null
+++ b/test/mppa/prng/README.md
@@ -0,0 +1,17 @@
+PRNG
+====
+
+This is a simple Pseudo Random Number Generator.
+
+`prng.c` contains a simple unitary test that compares the sum of the "bytewise sum"
+of 1000 generated numbers to a hardcoded result, that is the one obtained with
+`gcc -O2` on a x86 processor, and returns 0 if the result is correct.
+
+The following commands can be run inside that folder:
+
+- `make`: produces the unitary test binaries
+  - `prng-test-gcc-x86` : binary from gcc on x86
+  - `prng-test-k1c-x86` : binary from gcc on k1c
+  - `prng-test-ccomp-x86` : binary from ccomp on k1c
+- `make test`: tests the return value of the binaries produced by gcc.
+- `make check`: tests the return value of the binary produced by CompCert.
diff --git a/test/mppa/lib/prng.c b/test/mppa/prng/prng.c
index 59ec7ca6..71de1dc3 100644
--- a/test/mppa/lib/prng.c
+++ b/test/mppa/prng/prng.c
@@ -19,8 +19,9 @@ uint64_t randlong(void){
 #ifdef __UNIT_TEST_PRNG__
 char bytewise_sum(uint64_t to_check){
     char sum = 0;
+    int i;
 
-    for (int i = 0 ; i < 8 ; i++)
+    for (i = 0 ; i < 8 ; i++)
         sum += (to_check & (uint64_t)(0xFFULL << i*8)) >> i*8;
 
     return sum;
@@ -28,15 +29,13 @@ char bytewise_sum(uint64_t to_check){
 
 int main(void){
     srand(42);
+    int i;
 
-    if (bytewise_sum(0xdeadbeefb00b1355ULL) != 91)
-        return 1;
-
-    for (int i = 0 ; i < 1000 ; i++)
+    for (i = 0 ; i < 1000 ; i++)
         randlong();
 
     uint64_t last = randlong();
 
-    return !((unsigned char)bytewise_sum(last) == 251);
+    return !((unsigned char)bytewise_sum(last) == 155);
 }
 #endif // __UNIT_TEST_PRNG__
diff --git a/test/mppa/lib/prng.h b/test/mppa/prng/prng.h
index 6abdb45a..6abdb45a 100644
--- a/test/mppa/lib/prng.h
+++ b/test/mppa/prng/prng.h
diff --git a/test/mppa/lib/types.h b/test/mppa/prng/types.h
index 584023e3..584023e3 100644
--- a/test/mppa/lib/types.h
+++ b/test/mppa/prng/types.h
diff --git a/test/mppa/sort/.gitignore b/test/mppa/sort/.gitignore
index c8f4f4e5..a8d6921c 100644
--- a/test/mppa/sort/.gitignore
+++ b/test/mppa/sort/.gitignore
@@ -1,9 +1,9 @@
-insertion-test-k1c
-insertion-test-x86
-merge-test-k1c
-selection-test-k1c
-test-k1c
-merge-test-x86
-selection-test-x86
-test-x86
-test-ccomp
+main-test-ccomp-k1c
+main-test-gcc-k1c
+main-test-gcc-x86
+merge-test-gcc-k1c
+merge-test-gcc-x86
+selection-test-gcc-k1c
+selection-test-gcc-x86
+insertion-test-gcc-k1c
+insertion-test-gcc-x86
diff --git a/test/mppa/sort/Makefile b/test/mppa/sort/Makefile
index f94fe6b8..ebbad5b5 100644
--- a/test/mppa/sort/Makefile
+++ b/test/mppa/sort/Makefile
@@ -1,82 +1,91 @@
-PRNG=../lib/prng.c
-CCOMP=../../../ccomp
-
-ALL= insertion-test-x86 insertion-test-k1c\
-     selection-test-x86 selection-test-k1c\
-     merge-test-x86     merge-test-k1c\
-     test-x86           test-k1c\
-     test-ccomp
+K1CC ?= k1-mbr-gcc
+CC ?= gcc
+CCOMP ?= ccomp
+CFLAGS ?= -O2
+SIMU ?= k1-cluster
+TIMEOUT ?= 10s
+
+K1CCPATH=$(shell which $(K1CC))
+CCPATH=$(shell which $(CC))
+CCOMPPATH=$(shell which $(CCOMP))
+SIMUPATH=$(shell which $(SIMU))
+
+PRNG=../prng/prng.c
+
+CFILES=insertion.c merge.c selection.c main.c
+
+ALL= insertion-gcc-x86 insertion-gcc-k1c insertion-ccomp-k1c\
+     selection-gcc-x86 selection-gcc-k1c selection-ccomp-k1c\
+     merge-gcc-x86 merge-gcc-k1c merge-ccomp-k1c\
+     main-gcc-x86 main-gcc-k1c main-ccomp-k1c
+
+CCOMP_OUT= insertion-ccomp-k1c.out selection-ccomp-k1c.out merge-ccomp-k1c.out\
+		   main-ccomp-k1c.out
+GCC_OUT= insertion-gcc-k1c.out selection-gcc-k1c.out merge-gcc-k1c.out\
+		   main-gcc-k1c.out
+X86_GCC_OUT= insertion-gcc-x86.out selection-gcc-x86.out merge-gcc-x86.out\
+		   main-gcc-x86.out
+STUB_OUT= .zero
 
 all: $(ALL)
 
-%-test-x86: %.c $(PRNG)
-	gcc -g -D__UNIT_TEST_$$(echo $(basename $<) | tr a-z A-Z)__ -O2 -std=c99 $^ -o $@
-
-%-test-k1c: %.c $(PRNG)
-	k1-gcc -g -D__UNIT_TEST_$$(echo $(basename $<) | tr a-z A-Z)__ -O2 -std=c99 $^ -o $@
+main-gcc-x86: $(CFILES) $(PRNG) $(CCPATH)
+	$(CC) $(CFLAGS) $(filter-out $(CCPATH),$^) -o $@
 
-test-x86: selection.c merge.c insertion.c test.c $(PRNG)
-	gcc -g -O2 -std=c99 $^ -o $@
+%-gcc-x86: %.c $(PRNG) $(CCPATH)
+	$(CC) -D__UNIT_TEST_$$(echo $(basename $<) | tr a-z A-Z)__ $(CFLAGS) $(filter-out $(CCPATH),$^) -o $@
 
-test-k1c: selection.c merge.c insertion.c test.c $(PRNG)
-	k1-gcc -g -O2 -std=c99 $^ -o $@
+main-gcc-k1c: $(CFILES) $(PRNG) $(CCPATH)
+	$(K1CC) $(CFLAGS) $(filter-out $(CCPATH),$^) -o $@
 
-%.s: %.c $(CCOMP)
-	ccomp -O2 -S $< -o $@
+%-gcc-k1c: %.c $(PRNG) $(K1CCPATH)
+	$(K1CC) -D__UNIT_TEST_$$(echo $(basename $<) | tr a-z A-Z)__ $(CFLAGS) $(filter-out $(K1CCPATH),$^) -o $@
 
-test-ccomp: selection.s merge.s insertion.s test.s $(subst .c,.s,$(PRNG))
-	k1-gcc $^ -o $@
+main-ccomp-k1c: $(CFILES) $(PRNG) $(CCOMPPATH)
+	$(CCOMP) $(CFLAGS) $(filter-out $(CCOMPPATH),$^) -o $@
 
-.PHONY:
-unittest: unittest-x86 unittest-k1c
+%-ccomp-k1c: %.c $(PRNG) $(CCOMPPATH)
+	$(CCOMP) -D__UNIT_TEST_$$(echo $(basename $<) | tr a-z A-Z)__ $(CFLAGS) $(filter-out $(CCOMPPATH),$^) -o $@
 
-.PHONY:
-check: check-x86 check-k1c
+.SECONDARY:
+%x86.out: %x86
+	ret=0; timeout $(TIMEOUT) ./$< > $@ || { ret=$$?; }; echo $$ret >> $@
 
-.PHONY:
-compc-check: test-ccomp
-	@if ! k1-cluster -- ./$<; then\
-		>&2 echo "ERROR k1c: sort $< failed";\
-	else\
-		echo "k1c: Test sort $< succeeded";\
-	fi
-
-.PHONY:
-check-x86: test-x86
-	@if ! ./$<; then\
-		>&2 echo "ERROR x86: $< failed";\
-	else\
-		echo "x86: Test $< succeeded";\
-	fi
+%k1c.out: %k1c $(SIMUPATH)
+	ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@
 
-.PHONY:
-check-k1c: test-k1c
-	@if ! k1-cluster -- ./$<; then\
-		>&2 echo "ERROR k1c: $< failed";\
-	else\
-		echo "k1c: Test $< succeeded";\
-	fi
+.zero:
+	@echo "0" > $@
 
 .PHONY:
-unittest-x86: insertion-test-x86 selection-test-x86 merge-test-x86
-	@for test in $^; do\
-		if ! ./$$test; then\
+test-x86: $(STUB_OUT) $(X86_GCC_OUT)
+	@for test in $(wordlist 2,100,$^); do\
+		if ! diff $$test $(STUB_OUT); then\
 			>&2 echo "ERROR x86: $$test failed";\
 		else\
-			echo "x86: Test $$test Succeeded";\
+			echo "GOOD x86: $$test succeeded";\
 		fi;\
 	done
 
 .PHONY:
-unittest-k1c: insertion-test-k1c selection-test-k1c merge-test-k1c
-	@for test in $^; do\
-		if ! k1-cluster -- ./$$test; then\
+test-k1c: $(STUB_OUT) $(GCC_OUT)
+	@for test in $(wordlist 2,100,$^); do\
+		if ! diff $$test $(STUB_OUT); then\
 			>&2 echo "ERROR k1c: $$test failed";\
 		else\
-			echo "k1c: Test $$test Succeeded";\
+			echo "GOOD k1c: $$test succeeded";\
 		fi;\
 	done
 
 .PHONY:
-clean:
-	rm -f $(ALL)
+test: test-x86 test-k1c
+
+.PHONY:
+check: $(STUB_OUT) $(CCOMP_OUT)
+	@for test in $(wordlist 2,100,$^); do\
+		if ! diff $$test $(STUB_OUT); then\
+			>&2 echo "ERROR k1c: $$test failed";\
+		else\
+			echo "GOOD k1c: $$test succeeded";\
+		fi;\
+	done
diff --git a/test/mppa/sort/README.md b/test/mppa/sort/README.md
new file mode 100644
index 00000000..b4c2279b
--- /dev/null
+++ b/test/mppa/sort/README.md
@@ -0,0 +1,17 @@
+PRNG
+====
+
+This is a simple Pseudo Random Number Generator.
+
+`prng.c` contains a simple unitary test that compares the sum of the "bytewise sum"
+of 1000 generated numbers to a hardcoded result, that is the one obtained with
+`gcc -O2` on a x86 processor, and returns 0 if the result is correct.
+
+The following commands can be run inside that folder:
+
+- `make`: produces the unitary test binaries
+  - `prng-test-gcc-x86` : binary from gcc on x86
+  - `prng-test-k1c-x86` : binary from gcc on k1c
+  - `prng-test-ccomp-x86` : binary from ccomp on k1c
+- `make test`: tests the return value of the binaries produced by gcc.
+- `make check`: tests the return value of the binary produced by CompCert.
diff --git a/test/mppa/sort/insertion.c b/test/mppa/sort/insertion.c
index 88093b64..bca09599 100644
--- a/test/mppa/sort/insertion.c
+++ b/test/mppa/sort/insertion.c
@@ -1,5 +1,5 @@
-#include "../lib/prng.h"
-#include "../lib/types.h"
+#include "../prng/prng.h"
+#include "../prng/types.h"
 
 #ifdef __UNIT_TEST_INSERTION__
 #define SIZE 100
@@ -14,16 +14,18 @@ void swap_ins(uint64_t *a, uint64_t *b){
 }
 
 int insert_sort(uint64_t *res, const uint64_t *T){
+    int i, j;
+
     if (SIZE <= 0)
         return -1;
 
-    for (int i = 0 ; i < SIZE ; i++)
+    for (i = 0 ; i < SIZE ; i++)
         res[i] = T[i];
 
-    for (int i = 0 ; i < SIZE-1 ; i++){
+    for (i = 0 ; i < SIZE-1 ; i++){
         if (res[i] > res[i+1]){
             swap_ins(&res[i], &res[i+1]);
-            for (int j = i ; j > 0 ; j--)
+            for (j = i ; j > 0 ; j--)
                 if (res[j-1] > res[j])
                     swap_ins(&res[j-1], &res[j]);
         }
@@ -36,9 +38,10 @@ int insert_sort(uint64_t *res, const uint64_t *T){
 int main(void){
     uint64_t T[SIZE];
     uint64_t res[SIZE];
+    int i;
     srand(42);
 
-    for (int i = 0 ; i < SIZE ; i++)
+    for (i = 0 ; i < SIZE ; i++)
         T[i] = randlong();
 
     /* Sorting the table */
@@ -46,7 +49,7 @@ int main(void){
 
     /* Computing max(T) */
     uint64_t max = T[0];
-    for (int i = 1 ; i < SIZE ; i++)
+    for (i = 1 ; i < SIZE ; i++)
         if (T[i] > max)
             max = T[i];
 
diff --git a/test/mppa/sort/test.c b/test/mppa/sort/main.c
index e5e14fef..aef419aa 100644
--- a/test/mppa/sort/test.c
+++ b/test/mppa/sort/main.c
@@ -1,5 +1,5 @@
-#include "../lib/prng.h"
-#include "../lib/types.h"
+#include "../prng/prng.h"
+#include "../prng/types.h"
 
 #include "test.h"
 #include "insertion.h"
@@ -9,9 +9,10 @@
 int main(void){
     uint64_t T[SIZE];
     uint64_t res1[SIZE], res2[SIZE], res3[SIZE];
+    int i;
     srand(42);
 
-    for (int i = 0 ; i < SIZE ; i++)
+    for (i = 0 ; i < SIZE ; i++)
         T[i] = randlong();
 
     /* insertion sort */
@@ -24,7 +25,7 @@ int main(void){
     if (merge_sort(res3, T) < 0) return -3;
 
     /* We should have: res1[i] == res2[i] == res3[i] */
-    for (int i = 0 ; i < SIZE ; i++){
+    for (i = 0 ; i < SIZE ; i++){
         if (!(res1[i] == res2[i] && res2[i] == res3[i]))
             return -4;
     }
diff --git a/test/mppa/sort/merge.c b/test/mppa/sort/merge.c
index b2d41ce3..99f8ba85 100644
--- a/test/mppa/sort/merge.c
+++ b/test/mppa/sort/merge.c
@@ -1,5 +1,5 @@
-#include "../lib/prng.h"
-#include "../lib/types.h"
+#include "../prng/prng.h"
+#include "../prng/types.h"
 
 //https://en.wikipedia.org/wiki/Merge_sort
 
@@ -15,8 +15,8 @@ int min(int a, int b){
 
 void BottomUpMerge(const uint64_t *A, int iLeft, int iRight, int iEnd, uint64_t *B)
 {
-    int i = iLeft, j = iRight;
-    for (int k = iLeft; k < iEnd; k++) {
+    int i = iLeft, j = iRight, k;
+    for (k = iLeft; k < iEnd; k++) {
         if (i < iRight && (j >= iEnd || A[i] <= A[j])) {
             B[k] = A[i];
             i = i + 1;
@@ -30,18 +30,20 @@ void BottomUpMerge(const uint64_t *A, int iLeft, int iRight, int iEnd, uint64_t
 void CopyArray(uint64_t *to, const uint64_t *from)
 {
     const int n = SIZE;
+    int i;
 
-    for(int i = 0; i < n; i++)
+    for(i = 0; i < n; i++)
         to[i] = from[i];
 }
 
 void BottomUpMergeSort(uint64_t *A, uint64_t *B)
 {
     const int n = SIZE;
+    int width, i;
 
-    for (int width = 1; width < n; width = 2 * width)
+    for (width = 1; width < n; width = 2 * width)
     {
-        for (int i = 0; i < n; i = i + 2 * width)
+        for (i = 0; i < n; i = i + 2 * width)
         {
             BottomUpMerge(A, i, min(i+width, n), min(i+2*width, n), B);
         }
@@ -50,12 +52,14 @@ void BottomUpMergeSort(uint64_t *A, uint64_t *B)
 }
 
 int merge_sort(uint64_t *res, const uint64_t *T){
+    int i;
+
     if (SIZE <= 0)
         return -1;
 
     uint64_t B[SIZE];
     uint64_t *A = res;
-    for (int i = 0 ; i < SIZE ; i++)
+    for (i = 0 ; i < SIZE ; i++)
         A[i] = T[i];
 
     BottomUpMergeSort(A, B);
@@ -67,9 +71,10 @@ int merge_sort(uint64_t *res, const uint64_t *T){
 int main(void){
     uint64_t T[SIZE];
     uint64_t res[SIZE];
+    int i;
     srand(42);
 
-    for (int i = 0 ; i < SIZE ; i++)
+    for (i = 0 ; i < SIZE ; i++)
         T[i] = randlong();
 
     /* Sorting the table */
@@ -77,7 +82,7 @@ int main(void){
 
     /* Computing max(T) */
     uint64_t max = T[0];
-    for (int i = 1 ; i < SIZE ; i++)
+    for (i = 1 ; i < SIZE ; i++)
         if (T[i] > max)
             max = T[i];
 
diff --git a/test/mppa/sort/selection.c b/test/mppa/sort/selection.c
index 89bc2c65..df4be04f 100644
--- a/test/mppa/sort/selection.c
+++ b/test/mppa/sort/selection.c
@@ -1,5 +1,5 @@
-#include "../lib/prng.h"
-#include "../lib/types.h"
+#include "../prng/prng.h"
+#include "../prng/types.h"
 
 #ifdef __UNIT_TEST_SELECTION__
 #define SIZE 100
@@ -14,15 +14,16 @@ void swap_sel(uint64_t *a, uint64_t *b){
 }
 
 int select_sort(uint64_t *res, const uint64_t *T){
+    int i, j, iMin;
+
     if (SIZE <= 0)
         return -1;
 
-    for (int i = 0 ; i < SIZE ; i++)
+    for (i = 0 ; i < SIZE ; i++)
         res[i] = T[i];
 
-    for (int j = 0 ; j < SIZE ; j++){
-        int i;
-        int iMin = j;
+    for (j = 0 ; j < SIZE ; j++){
+        iMin = j;
         for (i = j+1 ; i < SIZE ; i++)
             if (res[i] < res[iMin])
                 iMin = i;
@@ -38,17 +39,19 @@ int select_sort(uint64_t *res, const uint64_t *T){
 int main(void){
     uint64_t T[SIZE];
     uint64_t res[SIZE];
+    uint64_t max;
+    int i;
     srand(42);
 
-    for (int i = 0 ; i < SIZE ; i++)
+    for (i = 0 ; i < SIZE ; i++)
         T[i] = randlong();
 
     /* Sorting the table */
     if (select_sort(res, T) < 0) return -1;
 
     /* Computing max(T) */
-    uint64_t max = T[0];
-    for (int i = 1 ; i < SIZE ; i++)
+    max = T[0];
+    for (i = 1 ; i < SIZE ; i++)
         if (T[i] > max)
             max = T[i];
 
diff --git a/test/mppa/test.sh b/test/mppa/test.sh
new file mode 100755
index 00000000..dfeb153a
--- /dev/null
+++ b/test/mppa/test.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+# Tests the validity of the tests
+
+source do_test.sh
+
+do_test test