24 files changed, 126 insertions, 126 deletions
diff --git a/test/mppa/.gitignore b/test/mppa/.gitignore
index e8ebeff8..b10c40c8 100644
--- a/test/mppa/.gitignore
+++ b/test/mppa/.gitignore
@@ -6,15 +6,15 @@ prng/Makefile
 sort/Makefile
 prng/.zero
 sort/.zero
-sort/insertion-ccomp-k1c
-sort/insertion-gcc-k1c
+sort/insertion-ccomp-kvx
+sort/insertion-gcc-kvx
 sort/insertion-gcc-x86
-sort/main-ccomp-k1c
-sort/main-gcc-k1c
+sort/main-ccomp-kvx
+sort/main-gcc-kvx
 sort/main-gcc-x86
-sort/merge-ccomp-k1c
-sort/merge-gcc-k1c
+sort/merge-ccomp-kvx
+sort/merge-gcc-kvx
 sort/merge-gcc-x86
-sort/selection-ccomp-k1c
-sort/selection-gcc-k1c
+sort/selection-ccomp-kvx
+sort/selection-gcc-kvx
 sort/selection-gcc-x86
diff --git a/test/mppa/builtins/stsud.c b/test/mppa/builtins/stsud.c
index fb07b94f..fa42b001 100644
--- a/test/mppa/builtins/stsud.c
+++ b/test/mppa/builtins/stsud.c
@@ -2,6 +2,6 @@
 
 BEGIN_TEST_N(unsigned long long, 2)
 {
-    c = __builtin_k1_stsud(t[0], t[1]);
+    c = __builtin_kvx_stsud(t[0], t[1]);
 }
 END_TEST()
diff --git a/test/mppa/coverage.sh b/test/mppa/coverage.sh
index 42ed4182..96f6bc04 100755
--- a/test/mppa/coverage.sh
+++ b/test/mppa/coverage.sh
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-printer=../../mppa_k1c/TargetPrinter.ml
+printer=../../kvx/TargetPrinter.ml
 asmdir=instr/asm/
 to_cover_raw=/tmp/to_cover_raw
 to_cover=/tmp/to_cover
diff --git a/test/mppa/general/clzd.c b/test/mppa/general/clzd.c
index 4bedab97..d3e8a8ec 100644
--- a/test/mppa/general/clzd.c
+++ b/test/mppa/general/clzd.c
@@ -2,6 +2,6 @@
 
 BEGIN_TEST_N(unsigned long long, 1)
 {
-    c = __builtin_k1_clzd(t[0]);
+    c = __builtin_kvx_clzd(t[0]);
 }
 END_TEST()
diff --git a/test/mppa/general/clzw.c b/test/mppa/general/clzw.c
index 361492f2..7b5478fd 100644
--- a/test/mppa/general/clzw.c
+++ b/test/mppa/general/clzw.c
@@ -2,6 +2,6 @@
 
 BEGIN_TEST_N(unsigned long long, 1)
 {
-    c = __builtin_k1_clzw(t[0]);
+    c = __builtin_kvx_clzw(t[0]);
 }
 END_TEST()
diff --git a/test/mppa/general/ctzd.c b/test/mppa/general/ctzd.c
index 6f6586ad..bba869e1 100644
--- a/test/mppa/general/ctzd.c
+++ b/test/mppa/general/ctzd.c
@@ -2,6 +2,6 @@
 
 BEGIN_TEST_N(unsigned long long, 1)
 {
-    c = __builtin_k1_ctzd(t[0]);
+    c = __builtin_kvx_ctzd(t[0]);
 }
 END_TEST()
diff --git a/test/mppa/general/ctzw.c b/test/mppa/general/ctzw.c
index b0f2c937..a7128b04 100644
--- a/test/mppa/general/ctzw.c
+++ b/test/mppa/general/ctzw.c
@@ -2,6 +2,6 @@
 
 BEGIN_TEST_N(unsigned long long, 1)
 {
-    c = __builtin_k1_ctzw(t[0]);
+    c = __builtin_kvx_ctzw(t[0]);
 }
 END_TEST()
diff --git a/test/mppa/general/satd.c b/test/mppa/general/satd.c
index d8d0d256..9d0d1cf9 100644
--- a/test/mppa/general/satd.c
+++ b/test/mppa/general/satd.c
@@ -2,6 +2,6 @@
 
 BEGIN_TEST_N(unsigned long long, 2)
 {
-    c = __builtin_k1_satd(t[0], t[1]);
+    c = __builtin_kvx_satd(t[0], t[1]);
 }
 END_TEST()
diff --git a/test/mppa/general/sbmm8.c b/test/mppa/general/sbmm8.c
index beced8fc..91f13425 100644
--- a/test/mppa/general/sbmm8.c
+++ b/test/mppa/general/sbmm8.c
@@ -2,6 +2,6 @@
 
 BEGIN_TEST_N(unsigned long long, 2)
 {
-    c = __builtin_k1_sbmm8(t[0], t[1]);
+    c = __builtin_kvx_sbmm8(t[0], t[1]);
 }
 END_TEST()
diff --git a/test/mppa/general/sbmmt8.c b/test/mppa/general/sbmmt8.c
index 8a64e7e7..7b120dfa 100644
--- a/test/mppa/general/sbmmt8.c
+++ b/test/mppa/general/sbmmt8.c
@@ -2,6 +2,6 @@
 
 BEGIN_TEST_N(unsigned long long, 2)
 {
-    c = __builtin_k1_sbmmt8(t[0], t[1]);
+    c = __builtin_kvx_sbmmt8(t[0], t[1]);
 }
 END_TEST()
diff --git a/test/mppa/instr/Makefile b/test/mppa/instr/Makefile
index 37f7d0ab..e4f964b3 100644
--- a/test/mppa/instr/Makefile
+++ b/test/mppa/instr/Makefile
@@ -1,6 +1,6 @@
 SHELL := /bin/bash
 
-K1CC ?= k1-cos-gcc
+KVXC ?= k1-cos-gcc
 CC ?= gcc
 CCOMP ?= ccomp
 OPTIM ?= -O2
@@ -24,7 +24,7 @@ K1LIB=../lib/system.gcc.a
 #                    -> .ccomp.s -> .ccomp.bin -> .ccomp.out
 ##
 
-K1CCPATH=$(shell which $(K1CC))
+KVXCPATH=$(shell which $(KVXC))
 CCPATH=$(shell which $(CC))
 CCOMPPATH=$(shell which $(CCOMP))
 SIMUPATH=$(shell which $(SIMU))
@@ -63,8 +63,8 @@ simutest: $(X86_GCC_OUT) $(GCC_SIMUOUT)
 	for test in $(TESTNAMES); do\
 		x86out=$(OUTDIR)/$$test.x86-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";\
+		if grep "__KVX__" -q $$test.c; then\
+			printf "$(YELLOW)UNTESTED: $$test.c contains an \`#ifdef __KVX__\`\n";\
 		elif $(DIFF) $$x86out $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\
 			>&2 printf "$(RED)ERROR: $$x86out and $$gccout differ$(NC)\n";\
 		else\
@@ -91,8 +91,8 @@ hardtest: $(X86_GCC_OUT) $(GCC_HARDOUT)
 	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";\
+		if grep "__KVX__" -q $$test.c; then\
+			printf "$(YELLOW)UNTESTED: $$test.c contains an \`#ifdef __KVX__\`\n";\
 		elif $(DIFF) $$x86out $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\
 			>&2 printf "$(RED)ERROR: $$x86out and $$gccout differ$(NC)\n";\
 		else\
@@ -153,9 +153,9 @@ $(BINDIR)/%.x86-gcc.bin: $(ASMDIR)/%.x86-gcc.s $(LIB) $(CCPATH)
 	@mkdir -p $(@D)
 	$(CC) $(CFLAGS) $(filter-out $(CCPATH),$^) -o $@
 
-$(BINDIR)/%.gcc.bin: $(ASMDIR)/%.gcc.s $(K1LIB) $(K1CCPATH)
+$(BINDIR)/%.gcc.bin: $(ASMDIR)/%.gcc.s $(K1LIB) $(KVXCPATH)
 	@mkdir -p $(@D)
-	$(K1CC) $(CFLAGS) $(filter-out $(K1CCPATH),$^) -o $@
+	$(KVXC) $(CFLAGS) $(filter-out $(KVXCPATH),$^) -o $@
 
 $(BINDIR)/%.ccomp.bin: $(ASMDIR)/%.ccomp.s $(K1LIB) $(CCOMPPATH)
 	@mkdir -p $(@D)
@@ -167,9 +167,9 @@ $(ASMDIR)/%.x86-gcc.s: $(SRCDIR)/%.c $(CCPATH)
 	@mkdir -p $(@D)
 	$(CC) $(CFLAGS) -S $< -o $@
 
-$(ASMDIR)/%.gcc.s: $(SRCDIR)/%.c $(K1CCPATH)
+$(ASMDIR)/%.gcc.s: $(SRCDIR)/%.c $(KVXCPATH)
 	@mkdir -p $(@D)
-	$(K1CC) $(CFLAGS) -S $< -o $@
+	$(KVXC) $(CFLAGS) -S $< -o $@
 
 $(ASMDIR)/%.ccomp.s: $(SRCDIR)/%.c $(CCOMPPATH)
 	@mkdir -p $(@D)
diff --git a/test/mppa/instr/builtin32.c b/test/mppa/instr/builtin32.c
index c7689dc8..9efb33cd 100644
--- a/test/mppa/instr/builtin32.c
+++ b/test/mppa/instr/builtin32.c
@@ -2,9 +2,9 @@
 
 BEGIN_TEST(int)
   int *ptr = &c;
-#ifdef __K1C__
+#ifdef __KVX__
   int d = c;
-  a = __builtin_k1_alclrw(ptr);
+  a = __builtin_kvx_alclrw(ptr);
   c = d;
 
 #endif
diff --git a/test/mppa/instr/builtin64.c b/test/mppa/instr/builtin64.c
index dbbb1886..252eb2c6 100644
--- a/test/mppa/instr/builtin64.c
+++ b/test/mppa/instr/builtin64.c
@@ -2,16 +2,16 @@
 
 BEGIN_TEST(long long)
   long long *ptr = &c;
-#ifdef __K1C__
+#ifdef __KVX__
   long long d = c;
-  a = __builtin_k1_alclrd(ptr);
+  a = __builtin_kvx_alclrd(ptr);
   c = d;
   c += a;
 
   c += __builtin_clzll(a);
 
   /* Removed the AFADDD builtin who was incorrect in CompCert, see #157 */
-  // a = __builtin_k1_afaddd(ptr, a);
-  // a = __builtin_k1_afaddd(ptr, a);
+  // a = __builtin_kvx_afaddd(ptr, a);
+  // a = __builtin_kvx_afaddd(ptr, a);
 #endif
 END_TEST64()
diff --git a/test/mppa/interop/Makefile b/test/mppa/interop/Makefile
index 3a83d51c..a0d4d7da 100644
--- a/test/mppa/interop/Makefile
+++ b/test/mppa/interop/Makefile
@@ -1,6 +1,6 @@
 SHELL := /bin/bash
 
-K1CC ?= k1-cos-gcc
+KVXC ?= k1-cos-gcc
 CC ?= gcc
 CCOMP ?= ccomp
 CFLAGS ?= -O2 -Wno-varargs
@@ -26,7 +26,7 @@ VAARG_COMMON=vaarg_common
 # There is also a $(VAARG_COMMON) that is the same than $(COMMON) but with va_arg
 ##
 
-K1CCPATH=$(shell which $(K1CC))
+KVXCPATH=$(shell which $(KVXC))
 CCPATH=$(shell which $(CC))
 CCOMPPATH=$(shell which $(CCOMP))
 SIMUPATH=$(shell which $(SIMU))
@@ -273,9 +273,9 @@ $(BINDIR)/$(COMMON).x86-gcc.bin: $(OBJDIR)/$(COMMON).x86-gcc.o $(CCPATH)
 	@mkdir -p $(@D)
 	$(CC) $(CFLAGS) $< -o $@
 
-$(BINDIR)/$(COMMON).gcc.bin: $(OBJDIR)/$(COMMON).gcc.o $(K1CCPATH)
+$(BINDIR)/$(COMMON).gcc.bin: $(OBJDIR)/$(COMMON).gcc.o $(KVXCPATH)
 	@mkdir -p $(@D)
-	$(K1CC) $(CFLAGS) $< -o $@
+	$(KVXC) $(CFLAGS) $< -o $@
 
 $(BINDIR)/$(COMMON).ccomp.bin: $(OBJDIR)/$(COMMON).ccomp.o $(CCOMPPATH)
 	@mkdir -p $(@D)
@@ -287,9 +287,9 @@ $(BINDIR)/$(VAARG_COMMON).x86-gcc.bin: $(OBJDIR)/$(VAARG_COMMON).x86-gcc.o $(CCP
 	@mkdir -p $(@D)
 	$(CC) $(CFLAGS) $< -o $@
 
-$(BINDIR)/$(VAARG_COMMON).gcc.bin: $(OBJDIR)/$(VAARG_COMMON).gcc.o $(K1CCPATH)
+$(BINDIR)/$(VAARG_COMMON).gcc.bin: $(OBJDIR)/$(VAARG_COMMON).gcc.o $(KVXCPATH)
 	@mkdir -p $(@D)
-	$(K1CC) $(CFLAGS) $< -o $@
+	$(KVXC) $(CFLAGS) $< -o $@
 
 $(BINDIR)/$(VAARG_COMMON).ccomp.bin: $(OBJDIR)/$(VAARG_COMMON).ccomp.o $(CCOMPPATH)
 	@mkdir -p $(@D)
@@ -301,11 +301,11 @@ $(BINDIR)/%.x86-gcc.bin: $(OBJDIR)/%.x86-gcc.o $(OBJDIR)/$(COMMON).x86-gcc.o $(C
 	@mkdir -p $(@D)
 	$(CC) $(CFLAGS) $(wordlist 1,2,$^) -o $@
 
-$(BINDIR)/%.gcc.bin: $(OBJDIR)/%.gcc.o $(OBJDIR)/$(COMMON).gcc.o $(K1CCPATH)
+$(BINDIR)/%.gcc.bin: $(OBJDIR)/%.gcc.o $(OBJDIR)/$(COMMON).gcc.o $(KVXCPATH)
 	@mkdir -p $(@D)
-	$(K1CC) $(CFLAGS) $(wordlist 1,2,$^) -o $@
+	$(KVXC) $(CFLAGS) $(wordlist 1,2,$^) -o $@
 
-$(BINDIR)/%.gcc.rev.bin: $(OBJDIR)/%.gcc.o $(OBJDIR)/$(COMMON).ccomp.o $(K1CCPATH)
+$(BINDIR)/%.gcc.rev.bin: $(OBJDIR)/%.gcc.o $(OBJDIR)/$(COMMON).ccomp.o $(KVXCPATH)
 	@mkdir -p $(@D)
 	$(CCOMP) $(CFLAGS) $(wordlist 1,2,$^) -o $@
 
@@ -319,11 +319,11 @@ $(BINDIR)/%.x86-gcc.vaarg.bin: $(OBJDIR)/%.x86-gcc.o $(OBJDIR)/$(VAARG_COMMON).x
 	@mkdir -p $(@D)
 	$(CC) $(CFLAGS) $(wordlist 1,2,$^) -o $@
 
-$(BINDIR)/%.gcc.vaarg.bin: $(OBJDIR)/%.gcc.o $(OBJDIR)/$(VAARG_COMMON).gcc.o $(K1CCPATH)
+$(BINDIR)/%.gcc.vaarg.bin: $(OBJDIR)/%.gcc.o $(OBJDIR)/$(VAARG_COMMON).gcc.o $(KVXCPATH)
 	@mkdir -p $(@D)
-	$(K1CC) $(CFLAGS) $(wordlist 1,2,$^) -o $@
+	$(KVXC) $(CFLAGS) $(wordlist 1,2,$^) -o $@
 
-$(BINDIR)/%.gcc.rev.vaarg.bin: $(OBJDIR)/%.gcc.o $(OBJDIR)/$(VAARG_COMMON).ccomp.o $(K1CCPATH)
+$(BINDIR)/%.gcc.rev.vaarg.bin: $(OBJDIR)/%.gcc.o $(OBJDIR)/$(VAARG_COMMON).ccomp.o $(KVXCPATH)
 	@mkdir -p $(@D)
 	$(CCOMP) $(CFLAGS) $(wordlist 1,2,$^) -o $@
 
@@ -339,9 +339,9 @@ $(OBJDIR)/%.x86-gcc.o: $(ASMDIR)/%.x86-gcc.s $(CCPATH)
 	@mkdir -p $(@D)
 	$(CC) -c $(CFLAGS) $< -o $@
 
-$(OBJDIR)/%.gcc.o: $(ASMDIR)/%.gcc.s $(K1CCPATH)
+$(OBJDIR)/%.gcc.o: $(ASMDIR)/%.gcc.s $(KVXCPATH)
 	@mkdir -p $(@D)
-	$(K1CC) -c $(CFLAGS) $< -o $@
+	$(KVXC) -c $(CFLAGS) $< -o $@
 
 $(OBJDIR)/%.ccomp.o: $(ASMDIR)/%.ccomp.s $(CCOMPPATH)
 	@mkdir -p $(@D)
@@ -356,9 +356,9 @@ $(ASMDIR)/%.x86-gcc.s: $(SRCDIR)/%.c $(CCPATH)
 	@mkdir -p $(@D)
 	$(CC) $(CFLAGS) -S $< -o $@
 
-$(ASMDIR)/%.gcc.s: $(SRCDIR)/%.c $(K1CCPATH)
+$(ASMDIR)/%.gcc.s: $(SRCDIR)/%.c $(KVXCPATH)
 	@mkdir -p $(@D)
-	$(K1CC) $(CFLAGS) -S $< -o $@
+	$(KVXC) $(CFLAGS) -S $< -o $@
 
 $(ASMDIR)/%.ccomp.s: $(SRCDIR)/%.c $(CCOMPPATH)
 	@mkdir -p $(@D)
diff --git a/test/mppa/lib/Makefile b/test/mppa/lib/Makefile
index 08901db6..5a947bb3 100644
--- a/test/mppa/lib/Makefile
+++ b/test/mppa/lib/Makefile
@@ -1,4 +1,4 @@
-K1CC ?= k1-cos-gcc
+KVXC ?= k1-cos-gcc
 K1AR ?= k1-cos-ar
 CC ?= gcc
 AR ?= gcc-ar
@@ -14,7 +14,7 @@ BINDIR=$(DIR)/bin
 ASMDIR=$(DIR)/asm
 OBJDIR=$(DIR)/obj
 
-K1CCPATH=$(shell which $(K1CC))
+KVXCPATH=$(shell which $(KVXC))
 K1ARPATH=$(shell which $(K1AR))
 CCPATH=$(shell which $(CC))
 ARPATH=$(shell which $(AR))
@@ -89,9 +89,9 @@ $(BINDIR)/%.x86-gcc.bin: $(OBJDIR)/%.x86-gcc.o system.x86-gcc.a $(CCPATH)
 	@mkdir -p $(@D)
 	$(CC) $(CFLAGS) $(filter-out $(CCPATH),$^) -o $@
 
-$(BINDIR)/%.gcc.bin: $(OBJDIR)/%.gcc.o system.gcc.a $(K1CCPATH)
+$(BINDIR)/%.gcc.bin: $(OBJDIR)/%.gcc.o system.gcc.a $(KVXCPATH)
 	@mkdir -p $(@D)
-	$(K1CC) $(CFLAGS) $(filter-out $(K1CCPATH),$^) -o $@
+	$(KVXC) $(CFLAGS) $(filter-out $(KVXCPATH),$^) -o $@
 
 $(BINDIR)/%.ccomp.bin: $(OBJDIR)/%.ccomp.o system.gcc.a $(CCOMPPATH)
 	@mkdir -p $(@D)
@@ -110,9 +110,9 @@ $(OBJDIR)/%.x86-gcc.o: $(ASMDIR)/%.x86-gcc.s $(CCPATH)
 	@mkdir -p $(@D)
 	$(CC) $(CFLAGS) -c $< -o $@
 
-$(OBJDIR)/%.gcc.o: $(ASMDIR)/%.gcc.s $(K1CCPATH)
+$(OBJDIR)/%.gcc.o: $(ASMDIR)/%.gcc.s $(KVXCPATH)
 	@mkdir -p $(@D)
-	$(K1CC) $(CFLAGS) -c $< -o $@
+	$(KVXC) $(CFLAGS) -c $< -o $@
 
 $(OBJDIR)/%.ccomp.o: $(ASMDIR)/%.ccomp.s $(CCOMPPATH)
 	$(CCOMP) $(CFLAGS) -c $< -o $@
@@ -123,9 +123,9 @@ $(ASMDIR)/%.x86-gcc.s: $(SRCDIR)/%.c $(CCPATH)
 	@mkdir -p $(@D)
 	$(CC) $(CFLAGS) -S $< -o $@
 
-$(ASMDIR)/%.gcc.s: $(SRCDIR)/%.c $(K1CCPATH)
+$(ASMDIR)/%.gcc.s: $(SRCDIR)/%.c $(KVXCPATH)
 	@mkdir -p $(@D)
-	$(K1CC) $(CFLAGS) -S $< -o $@
+	$(KVXC) $(CFLAGS) -S $< -o $@
 
 $(ASMDIR)/%.ccomp.s: $(SRCDIR)/%.c $(CCOMPPATH)
 	@mkdir -p $(@D)
diff --git a/test/mppa/mmult/.gitignore b/test/mppa/mmult/.gitignore
index c9cd4c65..b43ccc5f 100644
--- a/test/mppa/mmult/.gitignore
+++ b/test/mppa/mmult/.gitignore
@@ -1,4 +1,4 @@
-mmult-test-ccomp-k1c
-mmult-test-gcc-k1c
+mmult-test-ccomp-kvx
+mmult-test-gcc-kvx
 mmult-test-gcc-x86
 .zero
diff --git a/test/mppa/mmult/Makefile b/test/mppa/mmult/Makefile
index 667faef8..e7cd890e 100644
--- a/test/mppa/mmult/Makefile
+++ b/test/mppa/mmult/Makefile
@@ -1,20 +1,20 @@
-K1CC ?= k1-cos-gcc
+KVXC ?= k1-cos-gcc
 CC ?= gcc
 CCOMP ?= ccomp
 CFLAGS ?= -O2
 SIMU ?= k1-mppa
 TIMEOUT ?= 10s
 
-K1CCPATH=$(shell which $(K1CC))
+KVXCPATH=$(shell which $(KVXC))
 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
+ALL= mmult-test-gcc-x86 mmult-test-gcc-kvx mmult-test-ccomp-kvx
+CCOMP_OUT= mmult-test-ccomp-kvx.out
+GCC_OUT= mmult-test-gcc-kvx.out
 X86_GCC_OUT= mmult-test-gcc-x86.out
 STUB_OUT=.zero
 
@@ -23,14 +23,14 @@ all: $(ALL)
 mmult-test-gcc-x86: mmult.c $(PRNG) $(CCPATH)
 	$(CC) $(CFLAGS) $(filter-out $(CCPATH),$^) -o $@
 
-mmult-test-gcc-k1c: mmult.c $(PRNG) $(K1CCPATH)
-	$(K1CC) $(CFLAGS) $(filter-out $(K1CCPATH),$^) -o $@
+mmult-test-gcc-kvx: mmult.c $(PRNG) $(KVXCPATH)
+	$(KVXC) $(CFLAGS) $(filter-out $(KVXCPATH),$^) -o $@
 
-mmult-test-ccomp-k1c: mmult.c $(PRNG) $(CCOMPPATH)
+mmult-test-ccomp-kvx: mmult.c $(PRNG) $(CCOMPPATH)
 	$(CCOMP) $(CFLAGS) $(filter-out $(CCOMPPATH),$^) -o $@
 
 .SECONDARY:
-%k1c.out: %k1c $(SIMUPATH)
+%kvx.out: %kvx $(SIMUPATH)
 	ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@
 
 %x86.out: %x86
@@ -40,7 +40,7 @@ mmult-test-ccomp-k1c: mmult.c $(PRNG) $(CCOMPPATH)
 	@echo "0" > $@
 
 .PHONY:
-test: test-x86 test-k1c
+test: test-x86 test-kvx
 
 .PHONY:
 test-x86: $(X86_GCC_OUT) $(STUB_OUT)
@@ -51,17 +51,17 @@ test-x86: $(X86_GCC_OUT) $(STUB_OUT)
 	fi
 
 .PHONY:
-test-k1c: $(GCC_OUT) $(STUB_OUT)
+test-kvx: $(GCC_OUT) $(STUB_OUT)
 	@if ! diff $< $(STUB_OUT); then\
-		>&2 echo "ERROR k1c: $< failed";\
+		>&2 echo "ERROR kvx: $< failed";\
 	else\
-		echo "GOOD k1c: $< succeeded";\
+		echo "GOOD kvx: $< succeeded";\
 	fi
 
 .PHONY:
 check: $(CCOMP_OUT) $(STUB_OUT)
 	@if ! diff $< $(STUB_OUT); then\
-		>&2 echo "ERROR k1c: $< failed";\
+		>&2 echo "ERROR kvx: $< failed";\
 	else\
-		echo "GOOD k1c: $< succeeded";\
+		echo "GOOD kvx: $< succeeded";\
 	fi
diff --git a/test/mppa/mmult/README.md b/test/mppa/mmult/README.md
index ef2bff7e..780603f6 100644
--- a/test/mppa/mmult/README.md
+++ b/test/mppa/mmult/README.md
@@ -11,7 +11,7 @@ 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
+  - `mmult-test-kvx-x86` : binary from gcc on kvx
+  - `mmult-test-ccomp-x86` : binary from ccomp on kvx
 - `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/prng/.gitignore b/test/mppa/prng/.gitignore
index 0792a78b..08023900 100644
--- a/test/mppa/prng/.gitignore
+++ b/test/mppa/prng/.gitignore
@@ -1,3 +1,3 @@
-prng-test-ccomp-k1c
+prng-test-ccomp-kvx
 prng-test-gcc-x86
-prng-test-gcc-k1c
+prng-test-gcc-kvx
diff --git a/test/mppa/prng/Makefile b/test/mppa/prng/Makefile
index 9cbb3872..68e5ffc9 100644
--- a/test/mppa/prng/Makefile
+++ b/test/mppa/prng/Makefile
@@ -1,18 +1,18 @@
-K1CC ?= k1-cos-gcc
+KVXC ?= k1-cos-gcc
 CC ?= gcc
 CCOMP ?= ccomp
 CFLAGS ?= -O2
 SIMU ?= k1-mppa
 TIMEOUT ?= 10s
 
-K1CCPATH=$(shell which $(K1CC))
+KVXCPATH=$(shell which $(KVXC))
 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
+ALL= prng-test-gcc-x86 prng-test-gcc-kvx prng-test-ccomp-kvx
+CCOMP_OUT= prng-test-ccomp-kvx.out
+GCC_OUT= prng-test-gcc-kvx.out
 X86_GCC_OUT= prng-test-gcc-x86.out
 STUB_OUT=.zero
 
@@ -21,14 +21,14 @@ 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-gcc-kvx: prng.c $(KVXCPATH)
+	$(KVXC) -D__UNIT_TEST_PRNG__ $(CFLAGS) $< -o $@
 
-prng-test-ccomp-k1c: prng.c $(CCOMPPATH)
+prng-test-ccomp-kvx: prng.c $(CCOMPPATH)
 	$(CCOMP) -D__UNIT_TEST_PRNG__ $(CFLAGS) $< -o $@
 
 .SECONDARY:
-%k1c.out: %k1c $(SIMUPATH)
+%kvx.out: %kvx $(SIMUPATH)
 	ret=0; timeout $(TIMEOUT) $(SIMU) -- $<  > $@ || { ret=$$?; }; echo $$ret >> $@
 
 %x86.out: %x86
@@ -38,7 +38,7 @@ prng-test-ccomp-k1c: prng.c $(CCOMPPATH)
 	@echo "0" > $@
 
 .PHONY:
-test: test-x86 test-k1c
+test: test-x86 test-kvx
 
 .PHONY:
 test-x86: $(X86_GCC_OUT) $(STUB_OUT)
@@ -49,21 +49,21 @@ test-x86: $(X86_GCC_OUT) $(STUB_OUT)
 	fi
 
 .PHONY:
-test-k1c: $(GCC_OUT) $(STUB_OUT)
+test-kvx: $(GCC_OUT) $(STUB_OUT)
 	@if ! diff $< $(STUB_OUT); then\
-		>&2 echo "ERROR k1c: $< failed";\
+		>&2 echo "ERROR kvx: $< failed";\
 	else\
-		echo "GOOD k1c: $< succeeded";\
+		echo "GOOD kvx: $< succeeded";\
 	fi
 
 .PHONY:
 check: $(CCOMP_OUT) $(STUB_OUT)
 	@if ! diff $< $(STUB_OUT); then\
-		>&2 echo "ERROR k1c: $< failed";\
+		>&2 echo "ERROR kvx: $< failed";\
 	else\
-		echo "GOOD k1c: $< succeeded";\
+		echo "GOOD kvx: $< succeeded";\
 	fi
 
 .PHONY:
 clean:
-	rm -f prng-test-gcc-x86 prng-test-gcc-k1c prng-test-ccomp-k1c
+	rm -f prng-test-gcc-x86 prng-test-gcc-kvx prng-test-ccomp-kvx
diff --git a/test/mppa/prng/README.md b/test/mppa/prng/README.md
index b4c2279b..98ed539d 100644
--- a/test/mppa/prng/README.md
+++ b/test/mppa/prng/README.md
@@ -11,7 +11,7 @@ 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
+  - `prng-test-kvx-x86` : binary from gcc on kvx
+  - `prng-test-ccomp-x86` : binary from ccomp on kvx
 - `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/.gitignore b/test/mppa/sort/.gitignore
index a8d6921c..070b87c4 100644
--- a/test/mppa/sort/.gitignore
+++ b/test/mppa/sort/.gitignore
@@ -1,9 +1,9 @@
-main-test-ccomp-k1c
-main-test-gcc-k1c
+main-test-ccomp-kvx
+main-test-gcc-kvx
 main-test-gcc-x86
-merge-test-gcc-k1c
+merge-test-gcc-kvx
 merge-test-gcc-x86
-selection-test-gcc-k1c
+selection-test-gcc-kvx
 selection-test-gcc-x86
-insertion-test-gcc-k1c
+insertion-test-gcc-kvx
 insertion-test-gcc-x86
diff --git a/test/mppa/sort/Makefile b/test/mppa/sort/Makefile
index 0ae9d1f6..c4090352 100644
--- a/test/mppa/sort/Makefile
+++ b/test/mppa/sort/Makefile
@@ -1,11 +1,11 @@
-K1CC ?= k1-cos-gcc
+KVXC ?= k1-cos-gcc
 CC ?= gcc
 CCOMP ?= ccomp
 CFLAGS ?= -O2
 SIMU ?= k1-mppa
 TIMEOUT ?= 10s
 
-K1CCPATH=$(shell which $(K1CC))
+KVXCPATH=$(shell which $(KVXC))
 CCPATH=$(shell which $(CC))
 CCOMPPATH=$(shell which $(CCOMP))
 SIMUPATH=$(shell which $(SIMU))
@@ -14,15 +14,15 @@ 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
+ALL= insertion-gcc-x86 insertion-gcc-kvx insertion-ccomp-kvx\
+     selection-gcc-x86 selection-gcc-kvx selection-ccomp-kvx\
+     merge-gcc-x86 merge-gcc-kvx merge-ccomp-kvx\
+     main-gcc-x86 main-gcc-kvx main-ccomp-kvx
 
-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
+CCOMP_OUT= insertion-ccomp-kvx.out selection-ccomp-kvx.out merge-ccomp-kvx.out\
+		   main-ccomp-kvx.out
+GCC_OUT= insertion-gcc-kvx.out selection-gcc-kvx.out merge-gcc-kvx.out\
+		   main-gcc-kvx.out
 X86_GCC_OUT= insertion-gcc-x86.out selection-gcc-x86.out merge-gcc-x86.out\
 		   main-gcc-x86.out
 STUB_OUT= .zero
@@ -35,23 +35,23 @@ main-gcc-x86: $(CFILES) $(PRNG) $(CCPATH)
 %-gcc-x86: %.c $(PRNG) $(CCPATH)
 	$(CC) -D__UNIT_TEST_$$(echo $(basename $<) | tr a-z A-Z)__ $(CFLAGS) $(filter-out $(CCPATH),$^) -o $@
 
-main-gcc-k1c: $(CFILES) $(PRNG) $(CCPATH)
-	$(K1CC) $(CFLAGS) $(filter-out $(CCPATH),$^) -o $@
+main-gcc-kvx: $(CFILES) $(PRNG) $(CCPATH)
+	$(KVXC) $(CFLAGS) $(filter-out $(CCPATH),$^) -o $@
 
-%-gcc-k1c: %.c $(PRNG) $(K1CCPATH)
-	$(K1CC) -D__UNIT_TEST_$$(echo $(basename $<) | tr a-z A-Z)__ $(CFLAGS) $(filter-out $(K1CCPATH),$^) -o $@
+%-gcc-kvx: %.c $(PRNG) $(KVXCPATH)
+	$(KVXC) -D__UNIT_TEST_$$(echo $(basename $<) | tr a-z A-Z)__ $(CFLAGS) $(filter-out $(KVXCPATH),$^) -o $@
 
-main-ccomp-k1c: $(CFILES) $(PRNG) $(CCOMPPATH)
+main-ccomp-kvx: $(CFILES) $(PRNG) $(CCOMPPATH)
 	$(CCOMP) $(CFLAGS) $(filter-out $(CCOMPPATH),$^) -o $@
 
-%-ccomp-k1c: %.c $(PRNG) $(CCOMPPATH)
+%-ccomp-kvx: %.c $(PRNG) $(CCOMPPATH)
 	$(CCOMP) -D__UNIT_TEST_$$(echo $(basename $<) | tr a-z A-Z)__ $(CFLAGS) $(filter-out $(CCOMPPATH),$^) -o $@
 
 .SECONDARY:
 %x86.out: %x86
 	ret=0; timeout $(TIMEOUT) ./$< > $@ || { ret=$$?; }; echo $$ret >> $@
 
-%k1c.out: %k1c $(SIMUPATH)
+%kvx.out: %kvx $(SIMUPATH)
 	ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@
 
 .zero:
@@ -68,24 +68,24 @@ test-x86: $(STUB_OUT) $(X86_GCC_OUT)
 	done
 
 .PHONY:
-test-k1c: $(STUB_OUT) $(GCC_OUT)
+test-kvx: $(STUB_OUT) $(GCC_OUT)
 	@for test in $(wordlist 2,100,$^); do\
 		if ! diff $$test $(STUB_OUT); then\
-			>&2 echo "ERROR k1c: $$test failed";\
+			>&2 echo "ERROR kvx: $$test failed";\
 		else\
-			echo "GOOD k1c: $$test succeeded";\
+			echo "GOOD kvx: $$test succeeded";\
 		fi;\
 	done
 
 .PHONY:
-test: test-x86 test-k1c
+test: test-x86 test-kvx
 
 .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";\
+			>&2 echo "ERROR kvx: $$test failed";\
 		else\
-			echo "GOOD k1c: $$test succeeded";\
+			echo "GOOD kvx: $$test succeeded";\
 		fi;\
 	done
diff --git a/test/mppa/sort/README.md b/test/mppa/sort/README.md
index b4c2279b..98ed539d 100644
--- a/test/mppa/sort/README.md
+++ b/test/mppa/sort/README.md
@@ -11,7 +11,7 @@ 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
+  - `prng-test-kvx-x86` : binary from gcc on kvx
+  - `prng-test-ccomp-x86` : binary from ccomp on kvx
 - `make test`: tests the return value of the binaries produced by gcc.
 - `make check`: tests the return value of the binary produced by CompCert.