<commit_before>#!/bin/sh
# regression tests for why3

REPLAYOPT=""

while test $# != 0; do
case "$1" in
  "--force")
        REPLAYOPT="$REPLAYOPT --force"
        ;;
  "--obsolete-only")
        REPLAYOPT="$REPLAYOPT --obsolete-only"
        ;;
  "--prover")
        REPLAYOPT="$REPLAYOPT --prover $2"
        shift
        ;;
  *)
        echo "$0: Unknown option '$1'"
        exit 2
esac
shift
done

TMP=$PWD/why3regtests.out
TMPERR=$PWD/why3regtests.err

cd `dirname $0`

# too early to do that
# REPLAYOPT="$REPLAYOPT --smoke-detector top"

res=0
export success=0
export total=0

run_dir () {
    for f in `ls $1/*/why3session.xml`; do
        d=`dirname $f`
	echo -n "Replaying $d ... "
        ../bin/why3replay.opt -q $REPLAYOPT $2 $d 2> $TMPERR > $TMP
        ret=$?
	if test "$ret" != "0"  ; then
	    echo -n "FAILED (ret code=$ret):"
            out=`head -1 $TMP`
            if test -z "$out" ; then
               echo "standard error: (standard output empty)"
               cat $TMPERR
            else
	       cat $TMP
            fi
	    res=1
	else
	    echo -n "OK"
	    cat $TMP $TMPERR
            success=`expr $success + 1`
	fi
        total=`expr $total + 1`
    done
}

echo "=== Standard Library ==="
run_dir ../lib/why3
echo ""

echo "=== Tests ==="
# there's no session there...
# run_dir tests
run_dir tests-provers
echo ""

echo "=== Check Builtin translation ==="
run_dir check-builtin
echo ""

echo "=== BTS ==="
run_dir bts
echo ""

echo "=== Logic ==="
run_dir logic
run_dir bitvectors "-I bitvectors"
echo ""

echo "=== Programs ==="
run_dir .
run_dir foveoos11-cm
run_dir hoare_logic
run_dir vacid_0_binary_heaps "-I vacid_0_binary_heaps"
echo ""

echo "Summary: $success/$total"
exit $res



<commit_msg>Fix obsolete calling convention.<commit_after>#!/bin/sh
# regression tests for why3

REPLAYOPT=""

while test $# != 0; do
case "$1" in
  "--force")
        REPLAYOPT="$REPLAYOPT --force"
        ;;
  "--obsolete-only")
        REPLAYOPT="$REPLAYOPT --obsolete-only"
        ;;
  "--prover")
        REPLAYOPT="$REPLAYOPT --prover $2"
        shift
        ;;
  *)
        echo "$0: Unknown option '$1'"
        exit 2
esac
shift
done

TMP=$PWD/why3regtests.out
TMPERR=$PWD/why3regtests.err

cd `dirname $0`

# too early to do that
# REPLAYOPT="$REPLAYOPT --smoke-detector top"

res=0
export success=0
export total=0

run_dir () {
    for f in `ls $1/*/why3session.xml`; do
        d=`dirname $f`
	echo -n "Replaying $d ... "
        ../bin/why3replay.opt -q $REPLAYOPT $2 $d 2> $TMPERR > $TMP
        ret=$?
	if test "$ret" != "0"  ; then
	    echo -n "FAILED (ret code=$ret):"
            out=`head -1 $TMP`
            if test -z "$out" ; then
               echo "standard error: (standard output empty)"
               cat $TMPERR
            else
	       cat $TMP
            fi
	    res=1
	else
	    echo -n "OK"
	    cat $TMP $TMPERR
            success=`expr $success + 1`
	fi
        total=`expr $total + 1`
    done
}

echo "=== Standard Library ==="
run_dir ../lib/why3
echo ""

echo "=== Tests ==="
# there's no session there...
# run_dir tests
run_dir tests-provers
echo ""

echo "=== Check Builtin translation ==="
run_dir check-builtin
echo ""

echo "=== BTS ==="
run_dir bts
echo ""

echo "=== Logic ==="
run_dir logic
run_dir bitvectors "-L bitvectors"
echo ""

echo "=== Programs ==="
run_dir .
run_dir foveoos11-cm
run_dir hoare_logic
run_dir vacid_0_binary_heaps "-L vacid_0_binary_heaps"
echo ""

echo "Summary: $success/$total"
exit $res




{'fraction_non_alphanumeric': 0.15312232677502138, 'fraction_numerical': 0.015968063872255488, 'mean_word_length': 2.2938967136150237, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 2}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '470280', 'n_tokens_mistral': 1309, 'n_tokens_neox': 1266, 'n_words': 353}