if test -e $os_skip_file && echo "$1" | grep -f "$os_skip_file" >/dev/null 2>&1; then
echo "=> $2: [skip os]"
echo >>$xml "<testcase classname='`xmlesc "$3"`' name='`xmlesc "$2"`' `timestamp`><skipped/></testcase>"
if test -e $os_skip_file && echo "$1" | grep -f "$os_skip_file" >/dev/null 2>&1; then
echo "=> $2: [skip os]"
echo >>$xml "<testcase classname='`xmlesc "$3"`' name='`xmlesc "$2"`' `timestamp`><skipped/></testcase>"
saferun -a -o "$ff.time.out" "$ff.bin" $args < "$inputs" > "$ff.res" 2>"$ff.err"
mv "$ff.time.out" "$ff.times.out"
awk '{ SUM += $1} END { print SUM }' "$ff.times.out" > "$ff.time.out"
saferun -a -o "$ff.time.out" "$ff.bin" $args < "$inputs" > "$ff.res" 2>"$ff.err"
mv "$ff.time.out" "$ff.times.out"
awk '{ SUM += $1} END { print SUM }' "$ff.times.out" > "$ff.time.out"