1 files changed, 31 insertions, 0 deletions
diff --git a/ccomp_profiling/prof_ci_tests.sh b/ccomp_profiling/prof_ci_tests.sh
new file mode 100755
index 00000000..9af2428a
--- /dev/null
+++ b/ccomp_profiling/prof_ci_tests.sh
@@ -0,0 +1,31 @@
+#!/bin/bash
+# @author gourdinl
+# Script to compute profiling results as csv from CI tests
+
+if [ $# -ne 2 ]; then
+    echo "Usage: ./prof_ci_tests.sh <root_dir> <fct1;fct2;...>"
+    echo $#
+    exit 1
+fi
+
+RDIR=$1
+RESULT=prof.csv
+JQ=jq
+CCOMP=$RDIR/ccomp
+TMP=$RDIR/json_tmp
+PROF_FCT=/home/yuki/Work/VERIMAG/Compcert_two/ccomp_profiling/prof_function.sh
+LANDMARKSFLAGS="on,format=json,output=temporary:$TMP,time"
+FCTS=$2
+
+cd $RDIR
+rm -rf $TMP
+mkdir $TMP
+make -C test clean
+export OCAML_LANDMARKS=$LANDMARKSFLAGS
+make -j4 -C test all_s
+echo "test_name,ratio_cycles,ratio_time" > $RESULT
+for file in $TMP/*; do
+  echo "Computing profiling results for $file"
+  RATIOS=$($PROF_FCT $JQ $file $FCTS | tail -n 1)
+  echo $RATIOS >> $RESULT
+done