update from BTL dev branch

1 files changed, 19 insertions, 0 deletions

diff --git a/ccomp_profiling/prof_multiple_ccomp.sh b/ccomp_profiling/prof_multiple_ccomp.sh
new file mode 100755
index 00000000..77a8bef7
--- /dev/null
+++ b/ccomp_profiling/prof_multiple_ccomp.sh
@@ -0,0 +1,19 @@
+#!/bin/bash
+# @author gourdinl
+# Script to compute profiling results for multiple version of CompCert
+
+CCOMPS=(
+  "/home/yuki/Work/VERIMAG/Compcert_one"
+  "/home/yuki/Work/VERIMAG/Compcert_two"
+  "/home/yuki/Work/VERIMAG/Compcert_three"
+)
+
+FCTS=(
+  '.*function_equiv_checker$;.*WF.*function_checker$;.*Live.*function_checker$'
+  '.*check_symbolic_simu$'
+  '.*check_symbolic_simu$;.*liveness_checker$'
+)
+
+for ((i = 0; i < ${#CCOMPS[@]}; i++)); do
+  ./prof_ci_tests.sh ${CCOMPS[$i]} ${FCTS[$i]}
+done