Merge branch 'mppa-work' into mppa-abstractbb-dev

48 files changed, 1458 insertions, 436 deletions

diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index e9b2610c..980e18f8 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -474,4 +474,106 @@ Proof.
     }
   }
 
-*)
\ No newline at end of file
+ *)
+
+Require Import Coq.ZArith.Zquot.
+Lemma Z_quot_pos_pos_bound: forall a b m,
+    0 <= a <= m -> 1 <= b -> 0 <= Z.quot a b <= m.
+Proof.
+  intros.
+  split.
+  { rewrite <- (Z.quot_0_l b) by omega.
+    apply Z_quot_monotone; omega.
+  }
+  apply Z.le_trans with (m := a).
+  {
+    apply Z_quot_le; tauto.
+  }
+  tauto.
+Qed.
+Lemma Z_quot_neg_pos_bound: forall a b m,
+    m <= a <= 0 -> 1 <= b -> m <= Z.quot a b <= 0.
+  intros.
+  assert (0 <= - (a ÷ b) <= -m).
+  {
+    rewrite <- Z.quot_opp_l by omega.
+    apply Z_quot_pos_pos_bound; omega.
+  }
+  omega.
+Qed.
+
+Lemma Z_quot_signed_pos_bound: forall a b,
+    Int.min_signed <= a <= Int.max_signed -> 1 <= b ->
+    Int.min_signed <= Z.quot a b <= Int.max_signed.
+Proof.
+  intros.
+  destruct (Z_lt_ge_dec a 0).
+  {
+    split.
+    { apply Z_quot_neg_pos_bound; omega. }
+    { eapply Z.le_trans with (m := 0).
+      { apply Z_quot_neg_pos_bound with (m := Int.min_signed); trivial.
+        split. tauto. auto with zarith.
+      }
+      discriminate.
+    }
+  }
+  { split.
+    { eapply Z.le_trans with (m := 0).
+      discriminate.
+      apply Z_quot_pos_pos_bound with (m := Int.max_signed); trivial.
+      split. omega. tauto.
+    }
+    { apply Z_quot_pos_pos_bound; omega.
+    }
+  }
+Qed.
+
+Lemma Z_quot_signed_neg_bound: forall a b,
+    Int.min_signed <= a <= Int.max_signed -> b < -1 ->
+    Int.min_signed <= Z.quot a b <= Int.max_signed.
+Proof.
+  change Int.min_signed with (-2147483648).
+  change Int.max_signed with 2147483647.
+  intros.
+
+  replace b with (-(-b)) by auto with zarith.
+  rewrite Z.quot_opp_r by omega.
+  assert (-2147483647 <= (a ÷ - b) <= 2147483648).
+  2: omega.
+  
+  destruct (Z_lt_ge_dec a 0).
+  {
+    replace a with (-(-a)) by auto with zarith.
+    rewrite Z.quot_opp_l by omega.
+    assert (-2147483648 <= - a ÷ - b <= 2147483647).
+    2: omega.
+    split.
+    {
+      rewrite Z.quot_opp_l by omega.
+      assert (a ÷ - b <= 2147483648).
+      2: omega.
+      {
+        apply Z.le_trans with (m := 0).
+        rewrite <- (Z.quot_0_l (-b)) by omega.
+        apply Z_quot_monotone; omega.
+        discriminate.
+      }
+    }
+    assert (- a ÷ - b < -a ).
+    2: omega.
+    apply Z_quot_lt; omega.
+  }
+  {
+    split.
+    { apply Z.le_trans with (m := 0).
+      discriminate.
+      rewrite <- (Z.quot_0_l (-b)) by omega.
+      apply Z_quot_monotone; omega.
+    }
+    { apply Z.le_trans with (m := a).
+      apply Z_quot_le.
+      all: omega.
+    }
+  }
+Qed.
diff --git a/test/monniaux/benches.sh b/test/monniaux/benches.sh
new file mode 100644
index 00000000..9bca6b42
--- /dev/null
+++ b/test/monniaux/benches.sh
@@ -0,0 +1 @@
+benches="binary_search bitsliced-aes bitsliced-tea complex float_mat glibc_qsort heapsort idea number_theoretic_transform quicksort sha-2 tacle-bench-lift tacle-bench-powerwindow ternary too_slow"
diff --git a/test/monniaux/binary_search/make.proto b/test/monniaux/binary_search/make.proto
index 19501e78..69f04092 100644
--- a/test/monniaux/binary_search/make.proto
+++ b/test/monniaux/binary_search/make.proto
@@ -1 +1 @@
-binary_search
+target: binary_search
diff --git a/test/monniaux/bitsliced-aes/Makefile b/test/monniaux/bitsliced-aes/Makefile
deleted file mode 100644
index 6a0367e0..00000000
--- a/test/monniaux/bitsliced-aes/Makefile
+++ /dev/null
@@ -1,23 +0,0 @@
-src = $(wildcard *.c) tests/tests.c
-
-include ../rules.mk
-
-all: test.gcc.k1c.out test.gcc.o1.k1c.out test.ccomp.k1c.out test.gcc.host.out test.ccomp.host.out
-
-test.gcc.o1.k1c: $(src:.c=.gcc.o1.k1c.o) ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+
-
-test.gcc.k1c: $(src:.c=.gcc.k1c.o) ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) -o $@ $+
-
-test.ccomp.k1c: $(src:.c=.ccomp.k1c.o) ../clock.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+
-
-test.gcc.host: $(src:.c=.gcc.host.o) ../clock.gcc.host.o
-	$(CC) $(CFLAGS) -o $@ $+
-
-test.ccomp.host: $(src:.c=.ccomp.host.o) ../clock.gcc.host.o
-	$(CCOMP) $(CCOMPFLAGS) -o $@ $+
-
-clean:
-	rm -f *.o *.k1c *.host */*.o *.s */*.s *.out
diff --git a/test/monniaux/bitsliced-aes/make.proto b/test/monniaux/bitsliced-aes/make.proto
new file mode 100644
index 00000000..530d7e36
--- /dev/null
+++ b/test/monniaux/bitsliced-aes/make.proto
@@ -0,0 +1,2 @@
+sources: "$(wildcard *.c) tests/tests.c"
+target: test
diff --git a/test/monniaux/bitsliced-tea/Makefile b/test/monniaux/bitsliced-tea/Makefile
deleted file mode 100644
index 3d5fd540..00000000
--- a/test/monniaux/bitsliced-tea/Makefile
+++ /dev/null
@@ -1,27 +0,0 @@
-include ../rules.mk
-
-PRODUCTS=bstea.gcc.host.out bstea.ccomp.host.out bstea.gcc.o1.k1c.out bstea.gcc.k1c.out bstea.ccomp.k1c.out bstea.ccomp.k1c.s bstea.gcc.k1c.s bstea.gcc.k1c bstea.ccomp.k1c bstea.gcc.host bstea.ccomp.host
-
-all:	$(PRODUCTS)
-
-bstea.gcc.host: bstea.c bstea_run.c bstea.h ../clock.o
-	$(CC) $(CFLAGS) bstea.c bstea_run.c ../clock.o -o $@
-
-bstea.ccomp.host: bstea.c bstea_run.c bstea.h ../clock.o
-	$(CCOMP) $(CCOMPFLAGS) bstea.c bstea_run.c ../clock.o -o $@
-
-bstea.gcc.k1c.s bstea.ccomp.k1c.s bstea_run.gcc.k1c.s: bstea.h
-
-bstea.gcc.k1c: bstea.gcc.k1c.o bstea_run.gcc.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-bstea.gcc.o1.k1c: bstea.gcc.o1.k1c.o bstea_run.gcc.o1.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@
-
-bstea.ccomp.k1c: bstea.ccomp.k1c.o bstea_run.gcc.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
-
-clean:
-	$(RM) -f *.k1c *.host *.out *.o *.s
-
-.PHONY: clean
diff --git a/test/monniaux/bitsliced-tea/make.proto b/test/monniaux/bitsliced-tea/make.proto
new file mode 100644
index 00000000..7ddc95d2
--- /dev/null
+++ b/test/monniaux/bitsliced-tea/make.proto
@@ -0,0 +1,2 @@
+objdeps: [{name: bstea_run, compiler: gcc}]
+target: bstea
diff --git a/test/monniaux/clean_benches.sh b/test/monniaux/clean_benches.sh
new file mode 100755
index 00000000..d246e110
--- /dev/null
+++ b/test/monniaux/clean_benches.sh
@@ -0,0 +1,7 @@
+
+source benches.sh
+
+rm -f commands.txt
+for bench in $benches; do
+  (cd $bench && make clean)
+done
diff --git a/test/monniaux/complex/Makefile b/test/monniaux/complex/Makefile
deleted file mode 100644
index ca3d441b..00000000
--- a/test/monniaux/complex/Makefile
+++ /dev/null
@@ -1,29 +0,0 @@
-include ../rules.mk
-
-PRODUCTS=complex_mat.gcc.host.out complex_mat.ccomp.host.out \
-	complex_mat.gcc.k1c.out complex_mat.gcc.o1.k1c.out complex_mat.ccomp.k1c.out \
-	complex_mat.gcc.k1c.s complex_mat.ccomp.k1c.s
-
-all:	$(PRODUCTS)
-
-complex_mat.gcc.host.s complex_mat.ccomp.host.s complex_mat.gcc.k1c.s complex_mat.ccomp.k1c.s : ../clock.h
-
-complex_mat.ccomp.host: complex_mat.ccomp.host.o ../clock.gcc.host.o
-	$(CCOMP) $(CCOMPFLAGS) $+ -o $@
-
-complex_mat.gcc.host: complex_mat.gcc.host.o ../clock.gcc.host.o
-	$(CC) $(CFLAGS) $+ -o $@
-
-complex_mat.gcc.k1c: complex_mat.gcc.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-complex_mat.gcc.o1.k1c: complex_mat.gcc.o1.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@
-
-complex_mat.ccomp.k1c: complex_mat.ccomp.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
-
-clean:
-	-rm -f *.o *.s *.k1c
-
-.PHONY: clean
diff --git a/test/monniaux/complex/make.proto b/test/monniaux/complex/make.proto
new file mode 100644
index 00000000..b4d1222f
--- /dev/null
+++ b/test/monniaux/complex/make.proto
@@ -0,0 +1 @@
+target: complex_mat
diff --git a/test/monniaux/float_mat/Makefile b/test/monniaux/float_mat/Makefile
deleted file mode 100644
index 0d3d68d6..00000000
--- a/test/monniaux/float_mat/Makefile
+++ /dev/null
@@ -1,24 +0,0 @@
-include ../rules.mk
-
-PRODUCTS=float_mat.host float_mat.gcc.o1.k1c.out float_mat.gcc.k1c.out float_mat.ccomp.k1c.out float_mat.ccomp.k1c.s float_mat.gcc.k1c.s float_mat.gcc.k1c float_mat.ccomp.k1c
-
-all:	$(PRODUCTS)
-
-float_mat.host: float_mat.c float_mat_run.c float_mat.h
-	$(CC) $(CFLAGS) float_mat.c float_mat_run.c -o $@
-
-float_mat.gcc.k1c.s float_mat.ccomp.k1c.s float_mat_run.gcc.k1c.s: float_mat.h
-
-float_mat.gcc.k1c: float_mat.gcc.k1c.o float_mat_run.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-float_mat.gcc.o1.k1c: float_mat.gcc.o1.k1c.o float_mat_run.gcc.o1.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@
-
-float_mat.ccomp.k1c: float_mat.ccomp.k1c.o float_mat_run.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
-
-clean:
-	$(RM) -f *.k1c *.host *.o *.s
-
-.PHONY: clean
diff --git a/test/monniaux/float_mat/make.proto b/test/monniaux/float_mat/make.proto
new file mode 100644
index 00000000..3628afbb
--- /dev/null
+++ b/test/monniaux/float_mat/make.proto
@@ -0,0 +1,2 @@
+objdeps: [{name: float_mat_run, compiler: gcc}]
+target: float_mat
diff --git a/test/monniaux/generate_makefiles.sh b/test/monniaux/generate_makefiles.sh
index ed8270b5..14a6bd92 100755
--- a/test/monniaux/generate_makefiles.sh
+++ b/test/monniaux/generate_makefiles.sh
@@ -1,5 +1,7 @@
 #!/usr/bin/bash
 
-for bench in binary_search; do
-  ./genmake.py $(cat $bench/make.proto) > $bench/Makefile
+source benches.sh
+
+for bench in $benches; do
+  ./genmake.py $bench/make.proto > $bench/Makefile
 done
diff --git a/test/monniaux/genmake.py b/test/monniaux/genmake.py
index 8503b1ee..c0fe0d05 100755
--- a/test/monniaux/genmake.py
+++ b/test/monniaux/genmake.py
@@ -9,6 +9,7 @@ See the source for more info.
 
 from collections import namedtuple
 import sys
+import yaml
 
 Optim = namedtuple("Optim", ["short", "full"])
 Env = namedtuple("Env", ["compiler", "optimizations", "target"])
@@ -31,8 +32,23 @@ environments = [gcc_x86, gcc_k1c, ccomp_x86, ccomp_k1c]
 # Argument parsing
 ##
 if len(sys.argv) != 2:
-  raise Exception("Only 1 argument should be given to this script")
-basename = sys.argv[1]
+  raise Exception("Only 1 argument should be given to this script: the make.proto file")
+yaml_file = sys.argv[1]
+
+with open(yaml_file, "r") as f:
+  settings = yaml.load(f.read())
+
+basename = settings["target"]
+objdeps = settings["objdeps"] if "objdeps" in settings else []
+intro = settings["intro"] if "intro" in settings else ""
+sources = settings["sources"] if "sources" in settings else None
+
+if sources:
+  intro += "\nsrc=" + sources
+
+for objdep in objdeps:
+  if objdep["compiler"] not in ("gcc", "ccomp", "both"):
+    raise Exception('Invalid compiler specified in make.proto:objdeps, should be either "gcc" or "ccomp" or "both"')
 
 ##
 # Printing the rules
@@ -41,35 +57,52 @@ basename = sys.argv[1]
 def make_product(env, optim):
   return basename + "." + env.compiler.short + (("." + optim.short) if optim.short != "" else "") + "." + env.target
 
+def make_obj(name, env, compiler_short):
+  return name + "." + compiler_short + "." + env.target + ".o"
+
 def make_clock(env, optim):
   return "clock.gcc." + env.target
 
+def make_sources(env, optim):
+  if sources:
+    return "$(src:.c=." + env.compiler.short + (("." + optim.short) if optim.short != "" else "") + "." + env.target + ".o)"
+  else:
+    return "{product}.o".format(product = make_product(env, optim))
+
 def print_rule(env, optim):
-  print("{product}: {product}.o ../{clock}.o"
-        .format(product = make_product(env, optim), clock = make_clock(env, optim)))
+  print("{product}: {sources} ../{clock}.o "
+        .format(product = make_product(env, optim),
+          sources = make_sources(env, optim), clock = make_clock(env, optim))
+          + " ".join([make_obj(objdep["name"], env, (objdep["compiler"] if objdep["compiler"] != "both" else env.compiler.short)) for objdep in objdeps]))
   print("	{compiler} {flags} $+ -o $@"
         .format(compiler = env.compiler.full, flags = optim.full))
 
 products = []
 for env in environments:
   for optim in env.optimizations:
-    products.append(make_product(env, optim) + ".out")
+    products.append(make_product(env, optim))
 
 print("""
 include ../rules.mk
 
-PRODUCTS?={}
+{intro}
+
+PRODUCTS?={prod}
+PRODUCTS_OUT=$(addsuffix .out,$(PRODUCTS))
 
 all: $(PRODUCTS)
-""".format(" ".join(products)))
+
+.PHONY:
+exec: $(PRODUCTS_OUT)
+
+""".format(intro=intro, prod=" ".join(products)))
 
 for env in environments:
   for optim in env.optimizations:
     print_rule(env, optim)
 
 print("""
+.PHONY:
 clean:
-	-rm -f *.o *.s *.k1c
-
-.PHONY: clean
+	rm -f *.o *.s *.k1c
 """)
diff --git a/test/monniaux/glibc_qsort/Makefile b/test/monniaux/glibc_qsort/Makefile
deleted file mode 100644
index 62902903..00000000
--- a/test/monniaux/glibc_qsort/Makefile
+++ /dev/null
@@ -1,27 +0,0 @@
-include ../rules.mk
-
-PRODUCTS=glibc_qsort.gcc.host.out glibc_qsort.ccomp.host.out glibc_qsort.gcc.k1c.out glibc_qsort.gcc.o1.k1c.out glibc_qsort.ccomp.k1c.out glibc_qsort.ccomp.k1c.s glibc_qsort.gcc.k1c.s glibc_qsort.gcc.k1c glibc_qsort.ccomp.k1c
-
-all:	$(PRODUCTS)
-
-glibc_qsort.gcc.host: glibc_qsort.c glibc_qsort_run.gcc.host.o glibc_qsort.h
-	$(CC) $(CFLAGS) glibc_qsort.c glibc_qsort_run.gcc.host.o -o $@
-
-glibc_qsort.ccomp.host: glibc_qsort.c glibc_qsort_run.gcc.host.o glibc_qsort.h
-	$(CCOMP) $(CCOMPFLAGS) glibc_qsort.c glibc_qsort_run.gcc.host.o -o $@
-
-glibc_qsort.gcc.k1c.s glibc_qsort.ccomp.k1c.s glibc_qsort_run.gcc.k1c.s: glibc_qsort.h
-
-glibc_qsort.gcc.k1c: glibc_qsort.gcc.k1c.o glibc_qsort_run.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-glibc_qsort.gcc.o1.k1c: glibc_qsort.gcc.o1.k1c.o glibc_qsort_run.gcc.o1.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@
-
-glibc_qsort.ccomp.k1c: glibc_qsort.ccomp.k1c.o glibc_qsort_run.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
-
-clean:
-	$(RM) -f $(PRODUCTS) glibc_qsort.gcc.k1c.o glibc_qsort.ccomp.k1c.o glibc_qsort_run.gcc.k1c.o glibc_qsort_run.gcc.k1c.s
-
-.PHONY: clean
diff --git a/test/monniaux/glibc_qsort/make.proto b/test/monniaux/glibc_qsort/make.proto
new file mode 100644
index 00000000..d89f9ea4
--- /dev/null
+++ b/test/monniaux/glibc_qsort/make.proto
@@ -0,0 +1,2 @@
+objdeps: [{name: glibc_qsort_run, compiler: gcc}]
+target: glibc_qsort
diff --git a/test/monniaux/heapsort/Makefile b/test/monniaux/heapsort/Makefile
deleted file mode 100644
index 74eb1dea..00000000
--- a/test/monniaux/heapsort/Makefile
+++ /dev/null
@@ -1,30 +0,0 @@
-include ../rules.mk
-
-PRODUCTS=heapsort.gcc.host.out heapsort.ccomp.host.out heapsort.gcc.o1.k1c.out heapsort.gcc.k1c.out heapsort.ccomp.k1c.out heapsort.ccomp.k1c.s heapsort.gcc.k1c.s heapsort.gcc.k1c heapsort.ccomp.k1c
-
-all:	$(PRODUCTS)
-
-heapsort.gcc.host: heapsort.c heapsort_run.gcc.host.o heapsort.h
-	$(CC) $(CFLAGS) heapsort.c heapsort_run.gcc.host.o -o $@
-
-heapsort.ccomp.host: heapsort.c heapsort_run.gcc.host.o heapsort.h
-	$(CCOMP) $(CCOMPFLAGS) heapsort.c heapsort_run.gcc.host.o -o $@
-
-heapsort.gcc.k1c.s heapsort.ccomp.k1c.s heapsort_run.gcc.k1c.s: heapsort.h
-
-heapsort.gcc.o1.k1c: heapsort.gcc.o1.k1c.o heapsort_run.gcc.o1.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@
-
-heapsort.gcc.k1c: heapsort.gcc.k1c.o heapsort_run.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-heapsort.ccomp.k1c: heapsort.ccomp.k1c.o heapsort_run.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
-
-%.k1c.out: %.k1c
-	k1-cluster --cycle-based -- $< | tee $@
-
-clean:
-	$(RM) -f $(PRODUCTS) heapsort.gcc.k1c.o heapsort.ccomp.k1c.o heapsort_run.gcc.k1c.o heapsort_run.gcc.k1c.s
-
-.PHONY: clean
diff --git a/test/monniaux/heapsort/make.proto b/test/monniaux/heapsort/make.proto
new file mode 100644
index 00000000..edbf0efd
--- /dev/null
+++ b/test/monniaux/heapsort/make.proto
@@ -0,0 +1,2 @@
+objdeps: [{name: heapsort_run, compiler: gcc}]
+target: heapsort
diff --git a/test/monniaux/idea/Makefile b/test/monniaux/idea/Makefile
deleted file mode 100644
index c638f22f..00000000
--- a/test/monniaux/idea/Makefile
+++ /dev/null
@@ -1,27 +0,0 @@
-include ../rules.mk
-
-PRODUCTS=idea.gcc.host.out idea.ccomp.host.out idea.gcc.o1.k1c.out idea.gcc.k1c.out idea.ccomp.k1c.out idea.ccomp.k1c.s idea.gcc.k1c.s idea.gcc.k1c idea.ccomp.k1c
-
-all:	$(PRODUCTS)
-
-idea.gcc.host: idea.c idea.h ../clock.gcc.host.o
-	$(CC) $(CFLAGS) idea.c ../clock.gcc.host.o -o $@
-
-idea.ccomp.host: idea.c idea.h ../clock.gcc.host.o
-	$(CCOMP) $(CCOMPFLAGS) idea.c ../clock.gcc.host.o -o $@
-
-idea.gcc.k1c.s idea.ccomp.k1c.s idea_run.gcc.k1c.s: idea.h
-
-idea.gcc.k1c: idea.gcc.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-idea.gcc.o1.k1c: idea.gcc.o1.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@
-
-idea.ccomp.k1c: idea.ccomp.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
-
-clean:
-	$(RM) -f $(PRODUCTS) idea.gcc.k1c.o idea.ccomp.k1c.o
-
-.PHONY: clean
diff --git a/test/monniaux/idea/make.proto b/test/monniaux/idea/make.proto
new file mode 100644
index 00000000..b633a3be
--- /dev/null
+++ b/test/monniaux/idea/make.proto
@@ -0,0 +1 @@
+target: idea
diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control.c b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.c
new file mode 100644
index 00000000..6025cd13
--- /dev/null
+++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.c
@@ -0,0 +1,342 @@
+#include <assert.h>
+#include "heater_control.h"
+
+/* C code generated by lustrec
+   Version number 1.6-@GITBRANCH@
+   Code is C99 compliant
+   Using (double) floating-point numbers */
+   
+/* Import dependencies */
+
+/* Global constants (definitions) */
+double FAILURE = -999.0;
+double TMIN = 6.0;
+double TMAX = 9.0;
+double DELTA = 0.5;
+
+/* Struct definitions */
+struct not_a_sauna2_mem {struct not_a_sauna2_reg {double __not_a_sauna2_2;
+                                                  } _reg; 
+                         struct _arrow_mem *ni_0;
+                         };
+struct heater_control_mem {struct heater_control_reg {_Bool __heater_control_16;
+                                                      } _reg; 
+                           struct _arrow_mem *ni_1;
+                           };
+struct not_a_sauna_mem {struct not_a_sauna_reg {double __not_a_sauna_2;
+                                                } _reg; 
+                        struct _arrow_mem *ni_2;
+                        };
+
+
+void not_a_sauna2_reset (struct not_a_sauna2_mem *self) {
+  
+  _arrow_reset(self->ni_0);
+  return;
+}
+
+void not_a_sauna2_step (double T, double T1, double T2, double T3,
+                        _Bool Heat_on, 
+                        _Bool (*ok),
+                        struct not_a_sauna2_mem *self) {
+  _Bool __not_a_sauna2_1;
+  
+  
+  _arrow_step (1, 0, &__not_a_sauna2_1, self->ni_0);
+  if (__not_a_sauna2_1) {
+    *ok = 1;
+  } else {
+    *ok = (self->_reg.__not_a_sauna2_2 < (9.0 - 6.0));
+  }
+  self->_reg.__not_a_sauna2_2 = T;
+  
+  return;
+}
+
+void heater_control_reset (struct heater_control_mem *self) {
+  
+  _arrow_reset(self->ni_1);
+  return;
+}
+
+void heater_control_step (double T, double T1, double T2, double T3, 
+                          _Bool (*Heat_on),
+                          struct heater_control_mem *self) {
+  double Median_42_max2_150_m;
+  double Median_42_max2_152_m;
+  double Median_42_min2_141_m;
+  double Median_42_min2_143_m;
+  double Median_52_max2_150_m;
+  double Median_52_max2_152_m;
+  double Median_52_min2_141_m;
+  double Median_52_min2_143_m;
+  double Tguess;
+  _Bool V12;
+  _Bool V13;
+  _Bool V23;
+  _Bool __heater_control_12;
+  double abs_15_a;
+  double abs_15_v;
+  double abs_23_a;
+  double abs_23_v;
+  double abs_7_a;
+  double abs_7_v;
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  abs_7_v = (T1 - T2);
+  if ((abs_7_v >= 0.0)) {
+    abs_7_a = abs_7_v;
+  } else {
+    abs_7_a = (- abs_7_v);
+  }
+  abs_23_v = (T2 - T3);
+  if ((abs_23_v >= 0.0)) {
+    abs_23_a = abs_23_v;
+  } else {
+    abs_23_a = (- abs_23_v);
+  }
+  abs_15_v = (T1 - T3);
+  if ((abs_15_v >= 0.0)) {
+    abs_15_a = abs_15_v;
+  } else {
+    abs_15_a = (- abs_15_v);
+  }
+  V23 = (abs_23_a < 0.5);
+  V13 = (abs_15_a < 0.5);
+  V12 = (abs_7_a < 0.5);
+  if ((T2 < T3)) {
+    Median_52_min2_141_m = T2;
+  } else {
+    Median_52_min2_141_m = T3;
+  }
+  if ((T2 > T3)) {
+    Median_42_max2_150_m = T2;
+  } else {
+    Median_42_max2_150_m = T3;
+  }
+  if ((T2 < T3)) {
+    Median_42_min2_141_m = T2;
+  } else {
+    Median_42_min2_141_m = T3;
+  }
+  if ((T2 > T3)) {
+    Median_52_max2_150_m = T2;
+  } else {
+    Median_52_max2_150_m = T3;
+  }
+  if ((T1 < Median_52_min2_141_m)) {
+    Median_52_min2_143_m = T1;
+  } else {
+    Median_52_min2_143_m = Median_52_min2_141_m;
+  }
+  if ((T1 > Median_52_max2_150_m)) {
+    Median_52_max2_152_m = T1;
+  } else {
+    Median_52_max2_152_m = Median_52_max2_150_m;
+  }
+  if ((T1 < Median_42_min2_141_m)) {
+    Median_42_min2_143_m = T1;
+  } else {
+    Median_42_min2_143_m = Median_42_min2_141_m;
+  }
+  if ((T1 > Median_42_max2_150_m)) {
+    Median_42_max2_152_m = T1;
+  } else {
+    Median_42_max2_152_m = Median_42_max2_150_m;
+  }
+  if ((((!V12) && (!V13)) && (!V23))) {
+    Tguess = -999.0;
+  } else {
+    if (((((V12 && (!V13)) && (!V23)) || ((V13 && (!V12)) && (!V23))) || ((V23 && (!V12)) && (!V13)))) {
+      Tguess = ((((T1 + T2) + T3) - Median_42_min2_143_m) - Median_42_max2_152_m);
+    } else {
+      if (((V12 && V13) && V23)) {
+        Tguess = ((((T1 + T2) + T3) - Median_52_min2_143_m) - Median_52_max2_152_m);
+      } else {
+        if (V12) {
+          Tguess = ((T1 + T2) / 2.0);
+        } else {
+          if (V13) {
+            Tguess = ((T1 + T3) / 2.0);
+          } else {
+            Tguess = ((T2 + T3) / 2.0);
+          }
+        }
+      }
+    }
+  }
+  _arrow_step (1, 0, &__heater_control_12, self->ni_1);
+  if (__heater_control_12) {
+    *Heat_on = 1;
+  } else {
+    if ((Tguess == -999.0)) {
+      *Heat_on = 0;
+    } else {
+      if ((Tguess < 6.0)) {
+        *Heat_on = 1;
+      } else {
+        if ((Tguess > 9.0)) {
+          *Heat_on = 0;
+        } else {
+          *Heat_on = self->_reg.__heater_control_16;
+        }
+      }
+    }
+  }
+  self->_reg.__heater_control_16 = *Heat_on;
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  return;
+}
+
+void not_a_sauna_reset (struct not_a_sauna_mem *self) {
+  
+  _arrow_reset(self->ni_2);
+  return;
+}
+
+void not_a_sauna_step (double T, double T1, double T2, double T3,
+                       _Bool Heat_on, 
+                       _Bool (*ok),
+                       struct not_a_sauna_mem *self) {
+  _Bool __not_a_sauna_1;
+  
+  
+  _arrow_step (1, 0, &__not_a_sauna_1, self->ni_2);
+  if (__not_a_sauna_1) {
+    *ok = 1;
+  } else {
+    *ok = (self->_reg.__not_a_sauna_2 < (9.0 + 1.0));
+  }
+  self->_reg.__not_a_sauna_2 = T;
+  
+  return;
+}
+
+void oneoftree_step (_Bool f1, _Bool f2, _Bool f3, 
+                     _Bool (*r)
+                     ) {
+  
+  *r = ((((f1 && (!f2)) && (!f3)) || ((f2 && (!f1)) && (!f3))) || ((f3 && (!f1)) && (!f2)));
+  return;
+}
+
+void noneoftree_step (_Bool f1, _Bool f2, _Bool f3, 
+                      _Bool (*r)
+                      ) {
+  
+  *r = (((!f1) && (!f2)) && (!f3));
+  return;
+}
+
+void alloftree_step (_Bool f1, _Bool f2, _Bool f3, 
+                     _Bool (*r)
+                     ) {
+  
+  *r = ((f1 && f2) && f3);
+  return;
+}
+
+void abs_step (double v, 
+               double (*a)
+               ) {
+  
+  if ((v >= 0.0)) {
+    *a = v;
+  } else {
+    *a = (- v);
+  }
+  return;
+}
+
+void Median_step (double a, double b, double c, 
+                  double (*z)
+                  ) {
+  double __Median_1;
+  double __Median_2;
+  double __Median_3;
+  double __Median_4;
+  
+  
+  
+  
+  
+  min2_step (b, c, &__Median_3);
+  min2_step (a, __Median_3, &__Median_4);
+  max2_step (b, c, &__Median_1);
+  max2_step (a, __Median_1, &__Median_2);
+  *z = ((((a + b) + c) - __Median_4) - __Median_2);
+  
+  
+  
+  
+  return;
+}
+
+void Average_step (double a, double b, 
+                   double (*z)
+                   ) {
+  
+  *z = ((a + b) / 2.0);
+  return;
+}
+
+void min2_step (double one, double two, 
+                double (*m)
+                ) {
+  
+  if ((one < two)) {
+    *m = one;
+  } else {
+    *m = two;
+  }
+  return;
+}
+
+void max2_step (double one, double two, 
+                double (*m)
+                ) {
+  
+  if ((one > two)) {
+    *m = one;
+  } else {
+    *m = two;
+  }
+  return;
+}
+
diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h
new file mode 100644
index 00000000..d25a7d52
--- /dev/null
+++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h
@@ -0,0 +1,96 @@
+/* C code generated by lustrec
+   Version number 1.6-@GITBRANCH@
+   Code is C99 compliant
+   Using (double) floating-point numbers */
+   
+#ifndef _HEATER_CONTROL
+#define _HEATER_CONTROL
+
+/* Imports standard library */
+#include <stdint.h>
+#include "/opt/lustrec/1.6/include/lustrec/arrow.h"
+
+
+/* Import dependencies */
+
+/* Types definitions */
+
+/* Global constant (declarations, definitions are in C file) */
+extern double FAILURE;
+extern double TMIN;
+extern double TMAX;
+extern double DELTA;
+
+/* Structs declarations */
+struct not_a_sauna2_mem;
+struct heater_control_mem;
+struct not_a_sauna_mem;
+
+/* Nodes declarations */
+extern void not_a_sauna2_reset (struct not_a_sauna2_mem *self);
+
+extern void not_a_sauna2_init (struct not_a_sauna2_mem *self);
+
+extern void not_a_sauna2_clear (struct not_a_sauna2_mem *self);
+
+extern void not_a_sauna2_step (double T, double T1, double T2, double T3,
+                               _Bool Heat_on, 
+                               _Bool (*ok),
+                               struct not_a_sauna2_mem *self);
+
+extern void heater_control_reset (struct heater_control_mem *self);
+
+extern void heater_control_init (struct heater_control_mem *self);
+
+extern void heater_control_clear (struct heater_control_mem *self);
+
+extern void heater_control_step (double T, double T1, double T2, double T3, 
+                                 _Bool (*Heat_on),
+                                 struct heater_control_mem *self);
+
+extern void not_a_sauna_reset (struct not_a_sauna_mem *self);
+
+extern void not_a_sauna_init (struct not_a_sauna_mem *self);
+
+extern void not_a_sauna_clear (struct not_a_sauna_mem *self);
+
+extern void not_a_sauna_step (double T, double T1, double T2, double T3,
+                              _Bool Heat_on, 
+                              _Bool (*ok),
+                              struct not_a_sauna_mem *self);
+
+extern void oneoftree_step (_Bool f1, _Bool f2, _Bool f3, 
+                            _Bool (*r)
+                            );
+
+extern void noneoftree_step (_Bool f1, _Bool f2, _Bool f3, 
+                             _Bool (*r)
+                             );
+
+extern void alloftree_step (_Bool f1, _Bool f2, _Bool f3, 
+                            _Bool (*r)
+                            );
+
+extern void abs_step (double v, 
+                      double (*a)
+                      );
+
+extern void Median_step (double a, double b, double c, 
+                         double (*z)
+                         );
+
+extern void Average_step (double a, double b, 
+                          double (*z)
+                          );
+
+extern void min2_step (double one, double two, 
+                       double (*m)
+                       );
+
+extern void max2_step (double one, double two, 
+                       double (*m)
+                       );
+
+
+#endif
+
diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control.lus b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.lus
new file mode 100644
index 00000000..9a668a47
--- /dev/null
+++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.lus
@@ -0,0 +1,126 @@
+--
+-- A fault-tolerant heater controller with 3 sensors.
+--
+-- To guess the temperature (T),
+--
+--    (1) It compares the value of the 3 sensors 2 by 2 to determine
+--      which ones seem are broken -- we consider then broken if they 
+--      differ too much.
+--
+--    (2) then, it performs a vote: 
+--        o If the tree sensors are broken, it does not heat;
+--        o If the temperature is bigger than TMAX, it does not  heat;
+--        o If the temperature is smaller than TMIN, it heats;
+--        o Otherwise, it keeps its previous state.
+
+
+const FAILURE = -999.0; -- a fake temperature given when all sensors are broken
+const TMIN = 6.0;
+const TMAX = 9.0;
+
+
+const DELTA = 0.5;
+-- const DELTA :  real;
+
+-----------------------------------------------------------------------
+-----------------------------------------------------------------------
+node heater_control(T, T1, T2, T3 : real) returns (Heat_on:bool);
+-- T is supposed to be the real temperature and is not
+-- used in the controller; we add it here in oder to test the 
+-- controller to be able to write a sensible oracle.
+
+
+var
+ V12,  V13,  V23 : bool;
+ Tguess : real;
+
+let
+  V12 = abs(T1-T2) < DELTA; -- Are T1 and T2 valid?
+  V13 = abs(T1-T3) < DELTA; -- Are T1 and T3 valid?
+  V23 = abs(T2-T3) < DELTA; -- Are T2 and T3 valid?
+
+  Tguess =
+    if noneoftree(V12, V13, V23) then FAILURE else
+    if oneoftree(V12, V13, V23) then Median(T1, T2, T3) else
+    if alloftree(V12, V13, V23) then Median(T1, T2, T3) else
+    -- 2 among V1, V2, V3 are false
+    if V12 then Average(T1, T2) else
+    if V13 then Average(T1, T3) else
+                -- V23 is necessarily true,  hence T1 is wrong
+                Average(T2, T3) ;
+
+  Heat_on = true -> 
+    if Tguess = FAILURE then false else
+    if Tguess < TMIN    then true  else
+    if Tguess > TMAX    then false else
+                        pre Heat_on;
+tel
+
+
+-----------------------------------------------------------------------
+-----------------------------------------------------------------------
+node not_a_sauna(T,  T1, T2, T3 : real; Heat_on: bool) returns (ok:bool);
+
+let
+  ok = true -> pre T < TMAX + 1.0 ;
+tel
+
+node not_a_sauna2(T,  T1, T2, T3 : real; Heat_on: bool) returns (ok:bool);
+
+let
+  ok = true -> pre T < TMAX - 6.0 ;
+tel
+
+
+
+-----------------------------------------------------------------------
+-----------------------------------------------------------------------
+
+-- returns the absolute value of 2 reals
+function abs (v : real) returns (a : real) ;
+let
+	a = if v >= 0.0 then v else -v ;
+tel
+
+-- returns the average values of 2 reals
+function Average(a, b: real) returns (z : real); 
+let 
+	z = (a+b)/2.0 ; 
+tel
+
+-- returns the median values of 3 reals
+function Median(a, b, c : real) returns (z : real); 
+let
+	z = a + b + c - min2 (a, min2(b,c)) - max2 (a, max2(b,c)) ;
+tel
+
+
+-- returns the maximum values of 2 reals
+function max2 (one, two  : real) returns (m : real) ;
+let
+	m = if one > two then one else two ;
+tel
+
+-- returns the minimum values of 2 reals
+function min2 (one, two  : real) returns (m : real) ;
+let
+	m = if one < two then one else two ;
+tel
+
+
+function noneoftree (f1, f2, f3 : bool) returns (r : bool) 
+let
+	 r = not f1 and not f2 and not f3 ;
+tel 
+
+function alloftree (f1, f2, f3 : bool) returns (r : bool) 
+let
+	 r =  f1 and f2 and f3 ;
+tel 
+
+function oneoftree (f1, f2, f3 : bool) returns (r : bool) 
+let
+	r = f1 and not f2 and not f3  or
+	    f2 and not f1 and not f3  or
+	    f3 and not f1 and not f2 ;
+tel
diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control_alloc.h b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_alloc.h
new file mode 100644
index 00000000..270ed4a3
--- /dev/null
+++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_alloc.h
@@ -0,0 +1,73 @@
+/* C code generated by lustrec
+   Version number 1.6-@GITBRANCH@
+   Code is C99 compliant
+   Using (double) floating-point numbers */
+   
+#ifndef _HEATER_CONTROL_alloc
+#define _HEATER_CONTROL_alloc
+
+/* Import header from heater_control */
+#include "heater_control.h"
+
+/* Import dependencies */
+
+/* Struct definitions */
+struct not_a_sauna2_mem {struct not_a_sauna2_reg {double __not_a_sauna2_2;
+                                                  } _reg; 
+                         struct _arrow_mem *ni_0;
+                         };
+struct heater_control_mem {struct heater_control_reg {_Bool __heater_control_16;
+                                                      } _reg; 
+                           struct _arrow_mem *ni_1;
+                           };
+struct not_a_sauna_mem {struct not_a_sauna_reg {double __not_a_sauna_2;
+                                                } _reg; 
+                        struct _arrow_mem *ni_2;
+                        };
+
+/* Node allocation function/macro prototypes */
+#define not_a_sauna2_DECLARE(attr, inst)\
+  attr struct not_a_sauna2_mem inst;\
+  _arrow_DECLARE(attr, inst ## _ni_0);
+  
+#define not_a_sauna2_LINK(inst) do {\
+  _arrow_LINK(inst ## _ni_0);\
+  inst.ni_0 = &inst ## _ni_0;\
+} while (0)
+
+#define not_a_sauna2_ALLOC(attr, inst)\
+  not_a_sauna2_DECLARE(attr, inst);\
+  not_a_sauna2_LINK(inst);
+
+
+#define heater_control_DECLARE(attr, inst)\
+  attr struct heater_control_mem inst;\
+  _arrow_DECLARE(attr, inst ## _ni_1);
+  
+#define heater_control_LINK(inst) do {\
+  _arrow_LINK(inst ## _ni_1);\
+  inst.ni_1 = &inst ## _ni_1;\
+} while (0)
+
+#define heater_control_ALLOC(attr, inst)\
+  heater_control_DECLARE(attr, inst);\
+  heater_control_LINK(inst);
+
+
+#define not_a_sauna_DECLARE(attr, inst)\
+  attr struct not_a_sauna_mem inst;\
+  _arrow_DECLARE(attr, inst ## _ni_2);
+  
+#define not_a_sauna_LINK(inst) do {\
+  _arrow_LINK(inst ## _ni_2);\
+  inst.ni_2 = &inst ## _ni_2;\
+} while (0)
+
+#define not_a_sauna_ALLOC(attr, inst)\
+  not_a_sauna_DECLARE(attr, inst);\
+  not_a_sauna_LINK(inst);
+
+
+
+#endif
+
diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c
new file mode 100644
index 00000000..d0298840
--- /dev/null
+++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c
@@ -0,0 +1,48 @@
+#include <stdio.h>
+#include <unistd.h>
+#include <stdlib.h>
+#include <assert.h>
+#include "heater_control_alloc.h"
+#include "../clock.h"
+#include "../dm_random.c"
+
+static double _get_double(void) {
+  return (dm_random_uint32()%70000U) * 1E-3 -20.0;
+}
+
+static void _put_bool(const char *name, _Bool b) {
+  printf("%s: %d\n", name, b);
+}
+
+/* C code generated by lustrec
+   Version number 1.6-@GITBRANCH@
+   Code is C99 compliant
+   Using (double) floating-point numbers */
+   
+int main (int argc, char *argv[]) {
+  
+  /* Main memory allocation */
+  heater_control_ALLOC(static,main_mem);
+
+  clock_prepare();
+  clock_start();
+  
+  /* Initialize the main memory */
+  heater_control_reset(&main_mem);
+  
+  /* Infinite loop */
+  for(int loop_count=0; loop_count<1000; loop_count++){
+    double T = _get_double();
+    double T1 = _get_double();
+    double T2 = _get_double();
+    double T3 = _get_double();
+    _Bool Heat_on;
+    heater_control_step (T, T1, T2, T3, &Heat_on, &main_mem);
+    // _put_bool("Heat_on", Heat_on);
+  }
+  
+  clock_stop();
+  print_total_clock();
+  
+  return 1;
+}
diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control.lus b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control.lus
new file mode 100644
index 00000000..9a668a47
--- /dev/null
+++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control.lus
@@ -0,0 +1,126 @@
+--
+-- A fault-tolerant heater controller with 3 sensors.
+--
+-- To guess the temperature (T),
+--
+--    (1) It compares the value of the 3 sensors 2 by 2 to determine
+--      which ones seem are broken -- we consider then broken if they 
+--      differ too much.
+--
+--    (2) then, it performs a vote: 
+--        o If the tree sensors are broken, it does not heat;
+--        o If the temperature is bigger than TMAX, it does not  heat;
+--        o If the temperature is smaller than TMIN, it heats;
+--        o Otherwise, it keeps its previous state.
+
+
+const FAILURE = -999.0; -- a fake temperature given when all sensors are broken
+const TMIN = 6.0;
+const TMAX = 9.0;
+
+
+const DELTA = 0.5;
+-- const DELTA :  real;
+
+-----------------------------------------------------------------------
+-----------------------------------------------------------------------
+node heater_control(T, T1, T2, T3 : real) returns (Heat_on:bool);
+-- T is supposed to be the real temperature and is not
+-- used in the controller; we add it here in oder to test the 
+-- controller to be able to write a sensible oracle.
+
+
+var
+ V12,  V13,  V23 : bool;
+ Tguess : real;
+
+let
+  V12 = abs(T1-T2) < DELTA; -- Are T1 and T2 valid?
+  V13 = abs(T1-T3) < DELTA; -- Are T1 and T3 valid?
+  V23 = abs(T2-T3) < DELTA; -- Are T2 and T3 valid?
+
+  Tguess =
+    if noneoftree(V12, V13, V23) then FAILURE else
+    if oneoftree(V12, V13, V23) then Median(T1, T2, T3) else
+    if alloftree(V12, V13, V23) then Median(T1, T2, T3) else
+    -- 2 among V1, V2, V3 are false
+    if V12 then Average(T1, T2) else
+    if V13 then Average(T1, T3) else
+                -- V23 is necessarily true,  hence T1 is wrong
+                Average(T2, T3) ;
+
+  Heat_on = true -> 
+    if Tguess = FAILURE then false else
+    if Tguess < TMIN    then true  else
+    if Tguess > TMAX    then false else
+                        pre Heat_on;
+tel
+
+
+-----------------------------------------------------------------------
+-----------------------------------------------------------------------
+node not_a_sauna(T,  T1, T2, T3 : real; Heat_on: bool) returns (ok:bool);
+
+let
+  ok = true -> pre T < TMAX + 1.0 ;
+tel
+
+node not_a_sauna2(T,  T1, T2, T3 : real; Heat_on: bool) returns (ok:bool);
+
+let
+  ok = true -> pre T < TMAX - 6.0 ;
+tel
+
+
+
+-----------------------------------------------------------------------
+-----------------------------------------------------------------------
+
+-- returns the absolute value of 2 reals
+function abs (v : real) returns (a : real) ;
+let
+	a = if v >= 0.0 then v else -v ;
+tel
+
+-- returns the average values of 2 reals
+function Average(a, b: real) returns (z : real); 
+let 
+	z = (a+b)/2.0 ; 
+tel
+
+-- returns the median values of 3 reals
+function Median(a, b, c : real) returns (z : real); 
+let
+	z = a + b + c - min2 (a, min2(b,c)) - max2 (a, max2(b,c)) ;
+tel
+
+
+-- returns the maximum values of 2 reals
+function max2 (one, two  : real) returns (m : real) ;
+let
+	m = if one > two then one else two ;
+tel
+
+-- returns the minimum values of 2 reals
+function min2 (one, two  : real) returns (m : real) ;
+let
+	m = if one < two then one else two ;
+tel
+
+
+function noneoftree (f1, f2, f3 : bool) returns (r : bool) 
+let
+	 r = not f1 and not f2 and not f3 ;
+tel 
+
+function alloftree (f1, f2, f3 : bool) returns (r : bool) 
+let
+	 r =  f1 and f2 and f3 ;
+tel 
+
+function oneoftree (f1, f2, f3 : bool) returns (r : bool) 
+let
+	r = f1 and not f2 and not f3  or
+	    f2 and not f1 and not f3  or
+	    f3 and not f1 and not f2 ;
+tel
diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.c b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.c
new file mode 100644
index 00000000..1b3cb947
--- /dev/null
+++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.c
@@ -0,0 +1,302 @@
+/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */
+/*  lv6 -en -2cgc heater_control.lus -n heater_control */
+/* on vanoise the 15/05/2019 at 13:20:10 */
+#include "heater_control_heater_control.h"
+//// Defining step functions
+// Memory initialisation for Lustre_arrow_ctx
+void Lustre_arrow_ctx_reset(Lustre_arrow_ctx_type* ctx){
+  int _i;
+  ctx->_memory = _true;
+}
+
+// Initialisation of the  internal structure of Lustre_arrow_ctx
+void Lustre_arrow_ctx_init(Lustre_arrow_ctx_type* ctx){
+  // ctx->client_data = cdata;
+  Lustre_arrow_ctx_reset(ctx);
+ }
+// Step function(s) for Lustre_arrow_ctx
+void Lustre_arrow_step(_boolean i1,_boolean i2,_boolean *out,Lustre_arrow_ctx_type* ctx){  *out = ((ctx->_memory)? i1 : i2);
+  ctx->_memory = _false;
+
+} // End of Lustre_arrow_step
+
+// Memory initialisation for Lustre_pre_ctx
+void Lustre_pre_ctx_reset(Lustre_pre_ctx_type* ctx){
+  int _i;
+
+}
+
+// Initialisation of the  internal structure of Lustre_pre_ctx
+void Lustre_pre_ctx_init(Lustre_pre_ctx_type* ctx){
+  // ctx->client_data = cdata;
+  Lustre_pre_ctx_reset(ctx);
+ }
+// Step function(s) for Lustre_pre_ctx
+void Lustre_pre_get(_boolean *out,Lustre_pre_ctx_type* ctx){
+  *out = ctx->_memory;
+
+} // End of Lustre_pre_get
+
+void Lustre_pre_set(_boolean i1,Lustre_pre_ctx_type* ctx){
+  ctx->_memory = i1;
+
+} // End of Lustre_pre_set
+
+// Step function(s) for Lustre_slash_ctx
+void Lustre_slash_step(_real i1,_real i2,_real *out){
+  *out = (i1 / i2);
+
+} // End of Lustre_slash_step
+
+// Memory initialisation for heater_control_heater_control_ctx
+void heater_control_heater_control_ctx_reset(heater_control_heater_control_ctx_type* ctx){
+  int _i;
+
+    Lustre_pre_ctx_reset(&ctx->Lustre_pre_ctx_tab[0]);
+    Lustre_arrow_ctx_reset(&ctx->Lustre_arrow_ctx_tab[0]);
+}
+
+// Initialisation of the  internal structure of heater_control_heater_control_ctx
+void heater_control_heater_control_ctx_init(heater_control_heater_control_ctx_type* ctx){
+  // ctx->client_data = cdata;
+  heater_control_heater_control_ctx_reset(ctx);
+ }
+// Step function(s) for heater_control_heater_control_ctx
+void heater_control_heater_control_step(_real T,_real T1,_real T2,_real T3,_boolean *Heat_on,heater_control_heater_control_ctx_type* ctx){   _boolean __split_9_3;
+   _real __split_10_3;
+   _boolean __split_9_2;
+   _real __split_10_2;
+   _boolean __split_9_1;
+   _real __split_10_1;
+   _real __split_1_3;
+   _real __split_1_2;
+   _real __split_1_1;
+   _real __split_2_2;
+   _real __split_3_2;
+   _real __split_4_2;
+   _real __split_5_2;
+   _real __split_6_2;
+   _real __split_7_2;
+   _real __split_8_2;
+   _boolean ___split_38_1_2;
+   _boolean ___split_38_2_2;
+   _boolean ___split_37_1_2;
+   _boolean ___split_37_2_2;
+   _boolean __split_11_1;
+   _real __split_2_1;
+   _real __split_3_1;
+   _real __split_4_1;
+   _real __split_5_1;
+   _real __split_6_1;
+   _real __split_7_1;
+   _real __split_8_1;
+   _boolean ___split_38_1_1;
+   _boolean ___split_38_2_1;
+   _boolean ___split_37_1_1;
+   _boolean ___split_37_2_1;
+   _boolean __split_43_1;
+   _boolean __split_44_1;
+   _boolean __split_45_1;
+   _boolean __split_46_1;
+   _boolean __split_47_1;
+   _boolean __split_48_1;
+   _boolean __split_49_1;
+   _boolean __split_50_1;
+   _boolean __split_51_1;
+   _boolean __split_52_1;
+   _boolean __split_53_1;
+   _boolean __split_54_1;
+   _boolean __split_55_1;
+   _boolean __split_39_1;
+   _boolean __split_40_1;
+   _boolean __split_41_1;
+   _boolean __split_42_1;
+   _boolean _split_36;
+   _boolean _split_35;
+   _boolean _split_34;
+   _boolean _split_33;
+   _boolean _split_32;
+   _boolean _split_31;
+   _boolean _split_30;
+   _real _split_29;
+   _real _split_28;
+   _real _split_27;
+   _real _split_26;
+   _real _split_25;
+   _real _split_24;
+   _real _split_23;
+   _real _split_22;
+   _boolean _split_21;
+   _real _split_20;
+   _boolean _split_19;
+   _boolean _split_18;
+   _real _split_17;
+   _real _split_16;
+   _real _split_15;
+   _real _split_14;
+   _real _split_13;
+   _real _split_12;
+   _boolean V12;
+   _boolean V13;
+   _boolean V23;
+   _real Tguess;
+
+  _split_16 = T2 - T3;
+  __split_10_1 = - _split_16;
+  __split_9_1 = _split_16 >= 0.0;
+   if (__split_9_1 == _true) {
+     _split_17 = _split_16;
+   } else {
+     _split_17 = __split_10_1;
+   }
+  V23 = _split_17 < 0.5;
+  __split_42_1 = ! V23;
+  _split_12 = T1 - T2;
+  __split_10_3 = - _split_12;
+  __split_9_3 = _split_12 >= 0.0;
+   if (__split_9_3 == _true) {
+     _split_13 = _split_12;
+   } else {
+     _split_13 = __split_10_3;
+   }
+  V12 = _split_13 < 0.5;
+  __split_39_1 = ! V12;
+  _split_14 = T1 - T3;
+  __split_10_2 = - _split_14;
+  __split_9_2 = _split_14 >= 0.0;
+   if (__split_9_2 == _true) {
+     _split_15 = _split_14;
+   } else {
+     _split_15 = __split_10_2;
+   }
+  V13 = _split_15 < 0.5;
+  __split_40_1 = ! V13;
+  __split_41_1 = __split_39_1 & __split_40_1;
+  _split_18 = __split_41_1 & __split_42_1;
+  __split_43_1 = ! V13;
+  __split_44_1 = V12 & __split_43_1;
+  __split_45_1 = ! V23;
+  __split_46_1 = __split_44_1 & __split_45_1;
+  __split_47_1 = ! V12;
+  __split_48_1 = V13 & __split_47_1;
+  __split_49_1 = ! V23;
+  __split_50_1 = __split_48_1 & __split_49_1;
+  __split_51_1 = __split_46_1 | __split_50_1;
+  __split_54_1 = ! V13;
+  __split_52_1 = ! V12;
+  __split_53_1 = V23 & __split_52_1;
+  __split_55_1 = __split_53_1 & __split_54_1;
+  _split_19 = __split_51_1 | __split_55_1;
+  ___split_37_1_1 = T2 > T3;
+   if (___split_37_1_1 == _true) {
+     __split_7_1 = T2;
+   } else {
+     __split_7_1 = T3;
+   }
+  ___split_37_2_1 = T1 > __split_7_1;
+   if (___split_37_2_1 == _true) {
+     __split_8_1 = T1;
+   } else {
+     __split_8_1 = __split_7_1;
+   }
+  ___split_38_1_1 = T2 < T3;
+   if (___split_38_1_1 == _true) {
+     __split_4_1 = T2;
+   } else {
+     __split_4_1 = T3;
+   }
+  ___split_38_2_1 = T1 < __split_4_1;
+   if (___split_38_2_1 == _true) {
+     __split_5_1 = T1;
+   } else {
+     __split_5_1 = __split_4_1;
+   }
+  __split_2_1 = T1 + T2;
+  __split_3_1 = __split_2_1 + T3;
+  __split_6_1 = __split_3_1 - __split_5_1;
+  _split_20 = __split_6_1 - __split_8_1;
+  __split_1_2 = T1 + T3;
+  Lustre_slash_step(__split_1_2,2.0,&_split_24); 
+  __split_1_3 = T2 + T3;
+  Lustre_slash_step(__split_1_3,2.0,&_split_25); 
+   if (V13 == _true) {
+     _split_26 = _split_24;
+   } else {
+     _split_26 = _split_25;
+   }
+  __split_1_1 = T1 + T2;
+  Lustre_slash_step(__split_1_1,2.0,&_split_23); 
+   if (V12 == _true) {
+     _split_27 = _split_23;
+   } else {
+     _split_27 = _split_26;
+   }
+  __split_11_1 = V12 & V13;
+  _split_21 = __split_11_1 & V23;
+  ___split_37_1_2 = T2 > T3;
+   if (___split_37_1_2 == _true) {
+     __split_7_2 = T2;
+   } else {
+     __split_7_2 = T3;
+   }
+  ___split_37_2_2 = T1 > __split_7_2;
+   if (___split_37_2_2 == _true) {
+     __split_8_2 = T1;
+   } else {
+     __split_8_2 = __split_7_2;
+   }
+  ___split_38_1_2 = T2 < T3;
+   if (___split_38_1_2 == _true) {
+     __split_4_2 = T2;
+   } else {
+     __split_4_2 = T3;
+   }
+  ___split_38_2_2 = T1 < __split_4_2;
+   if (___split_38_2_2 == _true) {
+     __split_5_2 = T1;
+   } else {
+     __split_5_2 = __split_4_2;
+   }
+  __split_2_2 = T1 + T2;
+  __split_3_2 = __split_2_2 + T3;
+  __split_6_2 = __split_3_2 - __split_5_2;
+  _split_22 = __split_6_2 - __split_8_2;
+   if (_split_21 == _true) {
+     _split_28 = _split_22;
+   } else {
+     _split_28 = _split_27;
+   }
+   if (_split_19 == _true) {
+     _split_29 = _split_20;
+   } else {
+     _split_29 = _split_28;
+   }
+   if (_split_18 == _true) {
+     Tguess = -999.0;
+   } else {
+     Tguess = _split_29;
+   }
+  _split_30 = Tguess == -999.0;
+  _split_31 = Tguess < 6.0;
+  Lustre_pre_get(&_split_33,&ctx->Lustre_pre_ctx_tab[0]); 
+  _split_32 = Tguess > 9.0;
+   if (_split_32 == _true) {
+     _split_34 = _false;
+   } else {
+     _split_34 = _split_33;
+   }
+   if (_split_31 == _true) {
+     _split_35 = _true;
+   } else {
+     _split_35 = _split_34;
+   }
+   if (_split_30 == _true) {
+     _split_36 = _false;
+   } else {
+     _split_36 = _split_35;
+   }
+  Lustre_arrow_step(_true,_split_36,Heat_on,&ctx->Lustre_arrow_ctx_tab[0]); 
+  Lustre_pre_set(*Heat_on,&ctx->Lustre_pre_ctx_tab[0]); 
+
+} // End of heater_control_heater_control_step
+
diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.h b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.h
new file mode 100644
index 00000000..bfe8df20
--- /dev/null
+++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.h
@@ -0,0 +1,30 @@
+/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */
+/*  lv6 -en -2cgc heater_control.lus -n heater_control */
+/* on vanoise the 15/05/2019 at 13:20:10 */
+
+#include <stdlib.h>
+#include <string.h>
+
+#include "lustre_types.h"
+#include "lustre_consts.h"
+
+#ifndef _heater_control_heater_control_H_FILE
+#define _heater_control_heater_control_H_FILE
+void Lustre_arrow_ctx_reset(Lustre_arrow_ctx_type* ctx);
+void Lustre_arrow_ctx_init(Lustre_arrow_ctx_type* ctx);
+void Lustre_arrow_step(_boolean ,_boolean ,_boolean *,Lustre_arrow_ctx_type*);
+
+void Lustre_pre_ctx_reset(Lustre_pre_ctx_type* ctx);
+void Lustre_pre_ctx_init(Lustre_pre_ctx_type* ctx);
+void Lustre_pre_get(_boolean *,Lustre_pre_ctx_type*);
+
+void Lustre_pre_set(_boolean ,Lustre_pre_ctx_type*);
+
+void Lustre_slash_step(_real ,_real ,_real *);
+
+void heater_control_heater_control_ctx_reset(heater_control_heater_control_ctx_type* ctx);
+void heater_control_heater_control_ctx_init(heater_control_heater_control_ctx_type* ctx);
+void heater_control_heater_control_step(_real ,_real ,_real ,_real ,_boolean *,heater_control_heater_control_ctx_type*);
+
+/////////////////////////////////////////////////
+#endif
diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control_loop.c b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control_loop.c
new file mode 100644
index 00000000..d1a01268
--- /dev/null
+++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control_loop.c
@@ -0,0 +1,63 @@
+/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */
+/*  lv6 -en -2cgc heater_control.lus -n heater_control */
+/* on vanoise the 15/05/2019 at 13:20:10 */
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <unistd.h>
+#include "../dm_random.c"
+#include "../clock.h"
+#include "heater_control_heater_control.h" 
+
+/* MACROS DEFINITIONS ****************/
+#ifndef TT
+#define TT "1"
+#endif
+#ifndef FF
+#define FF "0"
+#endif
+#ifndef BB
+#define BB "bottom"
+#endif
+#ifdef CKCHECK
+/* set this macro for testing output clocks */
+#endif
+
+/* Standard Input procedures **************/
+_real _get_real(char* n){
+  return (dm_random_uint32()%70000U) * 1E-3 -20.0;
+}
+/* Standard Output procedures **************/
+void _put_bool(char* n, _boolean b){
+  printf("%s: %d\n", n, b);
+}
+/* Main procedure *************************/
+int main(){
+  _real T;
+  _real T1;
+  _real T2;
+  _real T3;
+  _boolean Heat_on;
+  heater_control_heater_control_ctx_type ctx_struct;
+  heater_control_heater_control_ctx_type* ctx = &ctx_struct;
+
+  clock_prepare();
+  clock_start();
+  
+  heater_control_heater_control_ctx_init(ctx);
+
+  /* Main loop */
+  for(int step=0; step<1000; step++){
+     T = _get_real("T");
+     T1 = _get_real("T1");
+     T2 = _get_real("T2");
+     T3 = _get_real("T3");
+    heater_control_heater_control_step(T,T1,T2,T3,&Heat_on,ctx);
+    // _put_bool("Heat_on", Heat_on);
+  }
+
+  clock_stop();
+  print_total_clock();
+  
+  return 1; 
+}
diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.c b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.c
new file mode 100644
index 00000000..47bfb5f5
--- /dev/null
+++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.c
@@ -0,0 +1,4 @@
+/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */
+/*  lv6 -en -2cgc heater_control.lus -n heater_control */
+/* on vanoise the 15/05/2019 at 13:20:10 */
+#include "lustre_consts.h"
\ No newline at end of file
diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.h b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.h
new file mode 100644
index 00000000..c2f70459
--- /dev/null
+++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.h
@@ -0,0 +1,9 @@
+/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */
+/*  lv6 -en -2cgc heater_control.lus -n heater_control */
+/* on vanoise the 15/05/2019 at 13:20:10 */
+
+// Constant definitions 
+#define heater_control_DELTA 0.5
+#define heater_control_FAILURE -999.0
+#define heater_control_TMAX 9.0
+#define heater_control_TMIN 6.0
diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_types.h b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_types.h
new file mode 100644
index 00000000..7fdfa03e
--- /dev/null
+++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_types.h
@@ -0,0 +1,41 @@
+/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */
+/*  lv6 -en -2cgc heater_control.lus -n heater_control */
+/* on vanoise the 15/05/2019 at 13:20:10 */
+
+#ifndef _SOC2C_PREDEF_TYPES
+#define _SOC2C_PREDEF_TYPES
+typedef int _boolean;
+typedef int _integer;
+typedef char* _string;
+typedef double _real;
+typedef double _double;
+typedef float _float;
+#define _false 0
+#define _true 1
+#endif
+// end of _SOC2C_PREDEF_TYPES
+// User typedef 
+#ifndef _heater_control_heater_control_TYPES
+#define _heater_control_heater_control_TYPES
+#endif // enf of  _heater_control_heater_control_TYPES
+// Memoryless soc ctx typedef 
+// Memoryfull soc ctx typedef 
+/* Lustre_arrow_ctx */
+typedef struct {
+   /*Memory cell*/
+   _boolean _memory ;
+} Lustre_arrow_ctx_type;
+
+/* Lustre_pre_ctx */
+typedef struct {
+   /*Memory cell*/
+   _boolean _memory ;
+} Lustre_pre_ctx_type;
+
+/* heater_control_heater_control_ctx */
+typedef struct {
+   /*INSTANCES*/
+   Lustre_pre_ctx_type Lustre_pre_ctx_tab[1];
+   Lustre_arrow_ctx_type Lustre_arrow_ctx_tab[1];
+} heater_control_heater_control_ctx_type;
+
diff --git a/test/monniaux/number_theoretic_transform/Makefile b/test/monniaux/number_theoretic_transform/Makefile
deleted file mode 100644
index 701703e1..00000000
--- a/test/monniaux/number_theoretic_transform/Makefile
+++ /dev/null
@@ -1,25 +0,0 @@
-include ../rules.mk
-
-PRODUCTS=ntt.gcc.host.out ntt.ccomp.host.out ntt.gcc.o1.k1c.out ntt.gcc.k1c.out ntt.ccomp.k1c.out ntt.ccomp.k1c.s ntt.gcc.k1c.s ntt.gcc.k1c ntt.ccomp.k1c ntt.gcc.host ntt.ccomp.host
-
-all:	$(PRODUCTS)
-
-ntt.gcc.host: ntt.c ../clock.o
-	$(CC) $(CFLAGS) ntt.c ../clock.o -o $@
-
-ntt.ccomp.host: ntt.c ../clock.o
-	$(CCOMP) $(CCOMPFLAGS) ntt.c ../clock.o -o $@
-
-ntt.gcc.k1c: ntt.gcc.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-ntt.gcc.o1.k1c: ntt.gcc.o1.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@
-
-ntt.ccomp.k1c: ntt.ccomp.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
-
-clean:
-	$(RM) -f *.k1c *.host *.out *.o *.s
-
-.PHONY: clean
diff --git a/test/monniaux/number_theoretic_transform/make.proto b/test/monniaux/number_theoretic_transform/make.proto
new file mode 100644
index 00000000..2d3c7144
--- /dev/null
+++ b/test/monniaux/number_theoretic_transform/make.proto
@@ -0,0 +1 @@
+target: ntt
diff --git a/test/monniaux/quicksort/Makefile b/test/monniaux/quicksort/Makefile
deleted file mode 100644
index f753d916..00000000
--- a/test/monniaux/quicksort/Makefile
+++ /dev/null
@@ -1,36 +0,0 @@
-include ../rules.mk
-
-PRODUCTS=quicksort.host quicksort.gcc.o1.k1c.out quicksort.gcc.k1c.out quicksort.ccomp.k1c.out quicksort.ccomp.k1c.s quicksort.gcc.k1c.s quicksort.gcc.k1c quicksort.ccomp.k1c
-
-all:	$(PRODUCTS)
-
-%.gcc.k1c.s: %.c
-	$(K1C_CC) $(K1C_CFLAGS) -S $< -o $@
-
-%.gcc.k1c.o: %.gcc.k1c.s
-	$(K1C_CC) $(K1C_CFLAGS) -c $< -o $@
-
-%.ccomp.k1c.s: %.c
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) -S $< -o $@
-
-%.ccomp.k1c.o: %.ccomp.k1c.s
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) -c $< -o $@
-
-quicksort.host: quicksort.c quicksort_run.c quicksort.h
-	$(CC) $(CFLAGS) quicksort.c quicksort_run.c -o $@
-
-quicksort.gcc.k1c.s quicksort.ccomp.k1c.s quicksort_run.gcc.k1c.s: quicksort.h
-
-quicksort.gcc.k1c: quicksort.gcc.k1c.o quicksort_run.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-quicksort.gcc.o1.k1c: quicksort.gcc.o1.k1c.o quicksort_run.gcc.o1.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-quicksort.ccomp.k1c: quicksort.ccomp.k1c.o quicksort_run.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
-
-clean:
-	$(RM) -f $(PRODUCTS) quicksort.gcc.k1c.o quicksort.ccomp.k1c.o quicksort_run.gcc.k1c.o quicksort_run.gcc.k1c.s
-
-.PHONY: clean
diff --git a/test/monniaux/quicksort/make.proto b/test/monniaux/quicksort/make.proto
new file mode 100644
index 00000000..4af771e5
--- /dev/null
+++ b/test/monniaux/quicksort/make.proto
@@ -0,0 +1,2 @@
+objdeps: [{name: quicksort_run, compiler: gcc}]
+target: quicksort
diff --git a/test/monniaux/rules.mk b/test/monniaux/rules.mk
index ffbdac96..d098d1b2 100644
--- a/test/monniaux/rules.mk
+++ b/test/monniaux/rules.mk
@@ -1,5 +1,5 @@
 ALL_CCOMPFLAGS=-fno-unprototyped
-CCOMP=ccomp
+CCOMP=ccomp-x86
 CCOMPFLAGS=-g -O3 -Wall $(ALL_CCOMPFLAGS) $(ALL_CFLAGS)
 
 CFLAGS=-g -std=c99 -O3 -Wall -Wextra -Werror=implicit  $(ALL_CFLAGS)
diff --git a/test/monniaux/run_makefiles.sh b/test/monniaux/run_makefiles.sh
new file mode 100755
index 00000000..02123665
--- /dev/null
+++ b/test/monniaux/run_makefiles.sh
@@ -0,0 +1,9 @@
+
+source benches.sh
+
+rm -f commands.txt
+for bench in $benches; do
+  echo "(cd $bench && make -j5 $1)" >> commands.txt
+done
+
+cat commands.txt | xargs -n1 -I{} -P4 bash -c '{}'
diff --git a/test/monniaux/sha-2/Makefile b/test/monniaux/sha-2/Makefile
deleted file mode 100644
index 8fba819b..00000000
--- a/test/monniaux/sha-2/Makefile
+++ /dev/null
@@ -1,24 +0,0 @@
-include ../rules.mk
-
-PRODUCTS=sha-256.host sha-256.gcc.o1.k1c.out sha-256.gcc.k1c.out sha-256.ccomp.k1c.out sha-256.ccomp.k1c.s sha-256.gcc.k1c.s sha-256.gcc.k1c sha-256.ccomp.k1c
-
-all:	$(PRODUCTS)
-
-sha-256.host: sha-256.c sha-256_run.c sha-256.h
-	$(CC) $(CFLAGS) sha-256.c sha-256_run.c -o $@
-
-sha-256.gcc.k1c.s sha-256.ccomp.k1c.s sha-256_run.gcc.k1c.s: sha-256.h
-
-sha-256.gcc.k1c: sha-256.gcc.k1c.o sha-256_run.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-sha-256.gcc.o1.k1c: sha-256.gcc.o1.k1c.o sha-256_run.gcc.o1.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@
-
-sha-256.ccomp.k1c: sha-256.ccomp.k1c.o sha-256_run.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
-
-clean:
-	$(RM) -f $(PRODUCTS) sha-256.gcc.k1c.o sha-256.ccomp.k1c.o sha-256_run.gcc.k1c.o sha-256_run.gcc.k1c.s
-
-.PHONY: clean
diff --git a/test/monniaux/sha-2/make.proto b/test/monniaux/sha-2/make.proto
new file mode 100644
index 00000000..e96fee7d
--- /dev/null
+++ b/test/monniaux/sha-2/make.proto
@@ -0,0 +1,2 @@
+objdeps: [{name: sha-256_run, compiler: gcc}]
+target: sha-256
diff --git a/test/monniaux/tacle-bench-lift/Makefile b/test/monniaux/tacle-bench-lift/Makefile
deleted file mode 100644
index ab930adb..00000000
--- a/test/monniaux/tacle-bench-lift/Makefile
+++ /dev/null
@@ -1,42 +0,0 @@
-ALL_CFLAGS = -include kill_pragma.h
-
-CFILES=lift.c	liftlibcontrol.c  liftlibio.c
-
-HFILES=liftlibcontrol.h  liftlibio.h
-
-K1C_GCC_OFILES=$(CFILES:.c=.gcc.k1c.o)
-K1C_GCC_OFILES_O1=$(CFILES:.c=.gcc.o1.k1c.o)
-K1C_CCOMP_OFILES=$(CFILES:.c=.ccomp.k1c.o)
-K1C_GCC_SFILES=$(CFILES:.c=.gcc.k1c.s)
-K1C_CCOMP_SFILES=$(CFILES:.c=.ccomp.k1c.s)
-
-HOST_GCC_OFILES=$(CFILES:.c=.gcc.host.o)
-HOST_CCOMP_OFILES=$(CFILES:.c=.ccomp.host.o)
-HOST_GCC_SFILES=$(CFILES:.c=.gcc.host.s)
-HOST_CCOMP_SFILES=$(CFILES:.c=.ccomp.host.s)
-
-all:	lift.gcc.o1.k1c.out lift.gcc.k1c.out lift.ccomp.k1c.out $(K1C_GCC_SFILES) $(K1C_CCOMP_SFILES)
-
-include ../rules.mk
-
-$(K1C_GCC_SFILES) $(K1C_CCOMP_SFILES) $(HOST_GCC_SFILES) $(HOST_CCOMP_SFILES) : $(HFILES)
-
-lift.gcc.k1c: $(K1C_GCC_OFILES)
-	$(K1C_CC) $(K1C_CFLAGS) -o $@ $+ ../clock.gcc.k1c.o
-
-lift.gcc.o1.k1c: $(K1C_GCC_OFILES_O1)
-	$(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+ ../clock.gcc.k1c.o
-
-lift.ccomp.k1c: $(K1C_CCOMP_OFILES)
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+ ../clock.gcc.k1c.o
-
-lift.gcc.host: $(HOST_GCC_OFILES)
-	$(CC) $(CFLAGS) -o $@ $+ ../clock.gcc.host.o
-
-lift.ccomp.host: $(HOST_CCOMP_OFILES)
-	$(CCOMP) $(CCOMPFLAGS) -o $@ $+ ../clock.gcc.host.o
-
-.PHONY: clean
-
-clean:
-	rm -f *.s *.o *.k1c
diff --git a/test/monniaux/tacle-bench-lift/make.proto b/test/monniaux/tacle-bench-lift/make.proto
new file mode 100644
index 00000000..58dd5c39
--- /dev/null
+++ b/test/monniaux/tacle-bench-lift/make.proto
@@ -0,0 +1,3 @@
+intro: "ALL_CFLAGS = -include kill_pragma.h"
+objdeps: [{name: liftlibcontrol, compiler: both}, {name: liftlibio, compiler: both}]
+target: lift
diff --git a/test/monniaux/tacle-bench-powerwindow/Makefile b/test/monniaux/tacle-bench-powerwindow/Makefile
deleted file mode 100644
index 560a0cf9..00000000
--- a/test/monniaux/tacle-bench-powerwindow/Makefile
+++ /dev/null
@@ -1,48 +0,0 @@
-ALL_CFLAGS = -include kill_pragma.h
-
-CFILES=	powerwindow.c			powerwindow_PW_Control_DRV.c \
-	powerwindow_const_params.c	powerwindow_PW_Control_PSG_BackL.c \
-	powerwindow_controlexclusion.c	powerwindow_PW_Control_PSG_BackR.c \
-	powerwindow_debounce.c		powerwindow_PW_Control_PSG_Front.c \
-	powerwindow_inputs.c		wcclib.c \
-	powerwindow_powerwindow_control.c
-
-HFILES=	kill_pragma.h  wcclib.h \
-	$(wildcard powerwindow_HeaderFiles/*.h)
-
-K1C_GCC_OFILES=$(CFILES:.c=.gcc.k1c.o)
-K1C_GCC_OFILES_O1=$(CFILES:.c=.gcc.o1.k1c.o)
-K1C_CCOMP_OFILES=$(CFILES:.c=.ccomp.k1c.o)
-K1C_GCC_SFILES=$(CFILES:.c=.gcc.k1c.s)
-K1C_CCOMP_SFILES=$(CFILES:.c=.ccomp.k1c.s)
-
-HOST_GCC_OFILES=$(CFILES:.c=.gcc.host.o)
-HOST_CCOMP_OFILES=$(CFILES:.c=.ccomp.host.o)
-HOST_GCC_SFILES=$(CFILES:.c=.gcc.host.s)
-HOST_CCOMP_SFILES=$(CFILES:.c=.ccomp.host.s)
-
-all:	powerwindow.gcc.o1.k1c.out powerwindow.gcc.k1c.out powerwindow.ccomp.k1c.out $(K1C_GCC_SFILES) $(K1C_CCOMP_SFILES)
-
-include ../rules.mk
-
-$(K1C_GCC_SFILES) $(K1C_CCOMP_SFILES) $(HOST_GCC_SFILES) $(HOST_CCOMP_SFILES) : $(HFILES)
-
-powerwindow.gcc.k1c: $(K1C_GCC_OFILES)
-	$(K1C_CC) $(K1C_CFLAGS) -o $@ $+ ../clock.gcc.k1c.o
-
-powerwindow.gcc.o1.k1c: $(K1C_GCC_OFILES_O1)
-	$(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+ ../clock.gcc.k1c.o
-
-powerwindow.ccomp.k1c: $(K1C_CCOMP_OFILES)
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+ ../clock.gcc.k1c.o
-
-powerwindow.gcc.host: $(HOST_GCC_OFILES)
-	$(CC) $(CFLAGS) -o $@ $+ ../clock.gcc.host.o
-
-powerwindow.ccomp.host: $(HOST_CCOMP_OFILES)
-	$(CCOMP) $(CCOMPFLAGS) -o $@ $+ ../clock.gcc.host.o
-
-.PHONY: clean
-
-clean:
-	rm -f *.s *.o *.k1c
diff --git a/test/monniaux/tacle-bench-powerwindow/make.proto b/test/monniaux/tacle-bench-powerwindow/make.proto
new file mode 100644
index 00000000..3d1ad1e5
--- /dev/null
+++ b/test/monniaux/tacle-bench-powerwindow/make.proto
@@ -0,0 +1,7 @@
+intro: "ALL_CFLAGS = -include kill_pragma.h"
+objdeps: [{name: powerwindow_const_params, compiler: both}, {name: powerwindow_controlexclusion, compiler: both}, 
+          {name: powerwindow_debounce, compiler: both}, {name: powerwindow_inputs, compiler: both},
+          {name: powerwindow_powerwindow_control, compiler: both}, {name: powerwindow_PW_Control_DRV, compiler: both},
+          {name: powerwindow_PW_Control_PSG_BackL, compiler: both}, {name: powerwindow_PW_Control_PSG_BackR, compiler: both},
+          {name: powerwindow_PW_Control_PSG_Front, compiler: both}]
+target: powerwindow
diff --git a/test/monniaux/ternary/Makefile b/test/monniaux/ternary/Makefile
deleted file mode 100644
index 7b1fe155..00000000
--- a/test/monniaux/ternary/Makefile
+++ /dev/null
@@ -1,29 +0,0 @@
-include ../rules.mk
-
-PRODUCTS=ternary.gcc.host.out ternary.ccomp.host.out \
-	ternary.gcc.o1.k1c.out ternary.gcc.k1c.out ternary.ccomp.k1c.out \
-	ternary.gcc.k1c.s ternary.ccomp.k1c.s
-
-all:	$(PRODUCTS)
-
-ternary.gcc.host.s ternary.ccomp.host.s ternary.gcc.k1c.s ternary.ccomp.k1c.s : ../clock.h
-
-ternary.ccomp.host: ternary.ccomp.host.o ../clock.gcc.host.o
-	$(CCOMP) $(CCOMPFLAGS) $+ -o $@
-
-ternary.gcc.host: ternary.gcc.host.o ../clock.gcc.host.o
-	$(CC) $(CFLAGS) $+ -o $@
-
-ternary.gcc.k1c: ternary.gcc.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-ternary.gcc.o1.k1c: ternary.gcc.o1.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@
-
-ternary.ccomp.k1c: ternary.ccomp.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
-
-clean:
-	-rm -f *.o *.s *.k1c
-
-.PHONY: clean
diff --git a/test/monniaux/ternary/make.proto b/test/monniaux/ternary/make.proto
new file mode 100644
index 00000000..c5219f1c
--- /dev/null
+++ b/test/monniaux/ternary/make.proto
@@ -0,0 +1 @@
+target: ternary
diff --git a/test/monniaux/too_slow/Makefile b/test/monniaux/too_slow/Makefile
deleted file mode 100644
index fc612e2e..00000000
--- a/test/monniaux/too_slow/Makefile
+++ /dev/null
@@ -1,30 +0,0 @@
-include ../rules.mk
-
-PRODUCTS=memset_from_bitsliced-aes.gcc.host.out memset_from_bitsliced-aes.ccomp.host.out \
-	memset_from_bitsliced-aes.gcc.o1.k1c.out memset_from_bitsliced-aes.gcc.k1c.out memset_from_bitsliced-aes.ccomp.k1c.out \
-	memset_from_bitsliced-aes.gcc.k1c.s memset_from_bitsliced-aes.ccomp.k1c.s
-
-all:	$(PRODUCTS)
-
-memset_from_bitsliced-aes.gcc.host.s memset_from_bitsliced-aes.ccomp.host.s memset_from_bitsliced-aes.gcc.k1c.s memset_from_bitsliced-aes.ccomp.k1c.s : ../clock.h
-
-memset_from_bitsliced-aes.ccomp.host: memset_from_bitsliced-aes.ccomp.host.o ../clock.gcc.host.o
-	$(CCOMP) $(CCOMPFLAGS) $+ -o $@
-
-memset_from_bitsliced-aes.gcc.host: memset_from_bitsliced-aes.gcc.host.o ../clock.gcc.host.o
-	$(CC) $(CFLAGS) $+ -o $@
-
-memset_from_bitsliced-aes.gcc.k1c: memset_from_bitsliced-aes.gcc.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-memset_from_bitsliced-aes.gcc.o1.k1c: memset_from_bitsliced-aes.gcc.o1.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@
-
-memset_from_bitsliced-aes.ccomp.k1c: memset_from_bitsliced-aes.ccomp.k1c.o ../clock.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
-
-clean:
-	-rm -f *.o *.s *.k1c
-
-.PHONY: clean
-
diff --git a/test/monniaux/too_slow/make.proto b/test/monniaux/too_slow/make.proto
new file mode 100644
index 00000000..a7b0b37d
--- /dev/null
+++ b/test/monniaux/too_slow/make.proto
@@ -0,0 +1 @@
+target: memset_from_bitsliced-aes