use the old script to measure time

diff --git a/cdschecker_modified_benchmarks/test.sh b/cdschecker_modified_benchmarks/test.sh
index d5f92dceda44355468e9d5cf79f76f9e7193c311..3956b0e5727f58c4e87624b8ad1315c750c257b0 100755 (executable)
--- a/cdschecker_modified_benchmarks/test.sh
+++ b/cdschecker_modified_benchmarks/test.sh
@@ -6,21 +6,18 @@ COUNT_DATA_RACE=0
 COUNT_TIME=0
 
 for i in `seq 1 1 $TOTAL_RUN` ; do
-  OUTPUT="$( { time $EXE; } 2>&1 )"
+  OUTPUT="$(/usr/bin/time -f "time: %U %S" $EXE 2>&1)"
   RACE="$(echo "$OUTPUT" | grep "race")"
   if [ -n "$RACE" ] ; then
     ((++COUNT_DATA_RACE))
   fi
 
-  USER_TIME="$(echo "$OUTPUT" | grep -o "user..m.\....")"
-  USER_TIME_S="$(echo $USER_TIME | cut -d 'm' -f2 | cut -d '.' -f1)"
-  USER_TIME_MS="$(echo $USER_TIME | cut -d 'm' -f2 | cut -d '.' -f2)"
-
-  SYS_TIME="$(echo "$OUTPUT" | grep -o "sys..m.\....")"
-  SYS_TIME_S="$(echo $SYS_TIME | cut -d 'm' -f2 | cut -d '.' -f1)"
-  SYS_TIME_MS="$(echo $SYS_TIME | cut -d 'm' -f2 | cut -d '.' -f2)"
-
-  TIME_EXE=$((10#$USER_TIME_S * 1000 + 10#$USER_TIME_MS + 10#$SYS_TIME_S * 1000 + 10#$SYS_TIME_MS))
+  TIME="$(echo "$OUTPUT" | grep -o "time: .\... .\...")"
+  TIME_USER_S="$(echo "$TIME" | cut -d' ' -f2 | cut -d'.' -f1)"
+  TIME_USER_CS="$(echo "$TIME" | cut -d' ' -f2 | cut -d'.' -f2)"
+  TIME_SYSTEM_S="$(echo "$TIME" | cut -d' ' -f3 | cut -d'.' -f1)"
+  TIME_SYSTEM_CS="$(echo "$TIME" | cut -d' ' -f3 | cut -d'.' -f2)"
+  TIME_EXE=$((10#$TIME_USER_S * 1000 + 10#$TIME_USER_CS * 10 + 10#$TIME_SYSTEM_S * 1000 + 10#$TIME_SYSTEM_CS * 10))
   COUNT_TIME=$((COUNT_TIME + TIME_EXE))
 done