bench 3 KB
Newer Older
1 2 3 4
#!/bin/sh

# auto bench for why

MARCHE Claude's avatar
MARCHE Claude committed
5 6 7 8
# Useless in this script ?
# export WHY3LIB=lib
# export WHY3DATA=.

9
export WHY3LOADPATH=theories
10 11

pgm=$1
12
pgml=$2
13
pgml_options=
14 15 16 17 18 19 20 21

goods () {
    for f in $1/*.why; do
	echo -n "  "$f"... "
	base=$1/`basename $f .why`
	# running Why
	if ! $pgm $2 $f > /dev/null 2>&1; then
	    echo "why FAILED"
22 23 24
            echo "env: WHY3DATA='$WHY3DATA'"
            echo "invocation: $pgm $2 $f"
            echo "result:"
25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
	    $pgm $2 $f
	    exit 1
	fi
	echo "why ok... "
    done
}

bads () {
    for f in $1/*.why; do
	echo -n "  "$f"... "
	if $pgm $2 $f > /dev/null 2>&1; then 
	    echo "$pgm $2 $f"
	    echo "FAILED!"
	    exit 1 
        else 
	    echo "ok"
	fi
    done
}

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45 46 47 48
drivers () {
    for f in $1/*.drv; do
	echo -n "  "$f"... "
	# running Why
49
	if ! echo "theory Test goal G : 1=2 end" | $pgm -F why --driver $f - > /dev/null 2>&1; then
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
50
	    echo "why FAILED"
51
            echo "theory Test goal G : 1=2 end" | $pgm -F why --driver $f -
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
52 53 54 55 56 57
	    exit 1
	fi
	echo "why ok... "
    done
}

58 59 60
programs () {
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
MARCHE Claude's avatar
MARCHE Claude committed
61
	if ! $pgml -L modules $pgml_options $f $2 > /dev/null 2>&1; then 
62
	    echo 
MARCHE Claude's avatar
MARCHE Claude committed
63 64
	    echo "$pgml $pgml_options $f $2"
	    $pgml -L modules $pgml_options $f $2
65 66 67 68 69 70 71 72
	    echo "FAILED!"
	    exit 1 
        else 
	    echo "ok"
	fi
    done
}

73 74 75
bad_programs () {
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
76
	if $pgml -L modules $pgml_options $f > /dev/null 2>&1; then 
77 78 79 80 81 82 83 84 85 86
	    echo 
	    echo "$pgml $pgml_options $f"
	    echo "SHOULD FAIL!"
	    exit 1 
        else 
	    echo "ok"
	fi
    done
}

87 88 89
valid_goals () {
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
90
	if $pgml -L modules -P alt-ergo $f | grep -q -v Valid; then
91
	    echo "valid test $f failed!"
92
	    echo "$pgml -P alt-ergo $f"
93
	    $pgml -L modules -P alt-ergo $f
94 95 96 97 98 99 100
	    exit 1
       else 
	    echo "ok"
	fi
    done
}

MARCHE Claude's avatar
MARCHE Claude committed
101 102 103 104
echo "=== Checking drivers ==="
drivers drivers
echo ""

105
echo "=== Parsing good files  ==="
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
106
goods bench/typing/bad --parse-only
107 108 109
echo ""

echo "=== Type-checking bad files ==="
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
110
bads bench/typing/bad --type-only
111 112 113
echo ""

echo "=== Type-checking good files ==="
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
114
goods bench/typing/good --type-only
MARCHE Claude's avatar
MARCHE Claude committed
115 116
goods examples --type-only
goods examples/tptp --type-only
117 118
echo ""

119 120
echo "=== Type-checking theories ==="
goods theories --type-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
121 122
echo ""

123 124 125
echo "=== Parsing programs ==="
pgml_options=--parse-only
programs bench/programs/bad-typing
126
programs bench/programs/good
127 128 129 130 131 132 133 134
programs examples/programs
echo ""

echo "=== Type-checking bad programs ==="
pgml_options=--type-only
bad_programs bench/programs/bad-typing
echo ""

135 136 137 138 139
echo "=== Type-checking modules ==="
pgml_options=--type-only
programs modules
echo ""

140 141
echo "=== Type-checking good programs ==="
pgml_options=--type-only
142
programs bench/programs/good
143 144 145
programs examples/programs
echo ""

146 147 148
echo "=== VC generation on good programs ==="
pgml_options=
programs bench/programs/good
149
programs examples/programs
MARCHE Claude's avatar
MARCHE Claude committed
150
programs examples/programs/vacid_0_binary_heaps "-I examples/programs/vacid_0_binary_heaps"
151
echo ""
152

153 154 155 156
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""