Skip to content
Snippets Groups Projects
Commit 76bcbb97 authored by Basile Desloges's avatar Basile Desloges Committed by Andre Maroneze
Browse files

Add a possible parameter "all" for show_stats.sh

parent 658dae4c
No related branches found
No related tags found
1 merge request!61Add a possible parameter "all" for show_stats.sh
Pipeline #80084 failed
#!/bin/sh -eu
#!/bin/bash -eu
if [ $# -lt 2 ]; then
usage () {
echo "usage: $0 dir target1 [target2 ...]"
echo " or: $0 all"
exit 1
}
#if [ ( $# -lt 2 ) -o ( ( $# -eq 1 ) -a ( "$1" != "all" ) ) ]; then
if [ $# -lt 1 ]; then
usage
elif [ $# -eq 1 ] && [ "$1" != "all" ]; then
usage
fi
dir="$1"
......@@ -11,8 +19,31 @@ shift
# prevent issues with locale-specific numeric separators
LC_ALL=C
for target in "$@"; do
secs=$(grep '^user_time=' $dir/.frama-c/$target/stats.txt | cut -d= -f2-)
maxmem=$(grep '^memory=' $dir/.frama-c/$target/stats.txt | cut -d= -f2-)
printf "$dir/$target: user time %.2fs, memory %d KiB\n" $secs $maxmem
done
print_stats () {
local dir target secs maxmem stats_file
dir=$1
target=$2
stats_file="$dir/.frama-c/$target/stats.txt"
if [ -f "$stats_file" ]; then
secs=$(grep '^user_time=' "$stats_file" | cut -d= -f2-)
maxmem=$(grep '^memory=' "$stats_file" | cut -d= -f2-)
printf "$dir/$target: user time %.2fs, memory %d KiB\n" "$secs" "$maxmem"
fi
}
if [ "$dir" = "all" ]; then
SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
pushd "$SCRIPT_DIR" > /dev/null
find . -type d -path "./*/.frama-c/*.parse" -o -path "./*/.frama-c/*.eva" | \
cut -d/ -f2,4 | \
sort | \
while read -r dirtarget; do
IFS='/' read -r -a t <<< "$dirtarget"
print_stats "${t[0]}" "${t[1]}"
done
popd > /dev/null
else
for target in "$@"; do
print_stats "$dir" "$target"
done
fi
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment