aboutsummaryrefslogtreecommitdiffstats
path: root/ccomp_profiling/prof_multiple_ccomp.sh
diff options
context:
space:
mode:
Diffstat (limited to 'ccomp_profiling/prof_multiple_ccomp.sh')
-rwxr-xr-xccomp_profiling/prof_multiple_ccomp.sh19
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