bench 3.38 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
10 11

pgm=$1
12
pgml=$1
13
pgml_options=
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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:"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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
drivers  
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
drivers  
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
drivers  
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 -t 10 -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 -t 10 -P alt-ergo $f
94 95 96 97 98 99 100
	    exit 1
       else 
	    echo "ok"
	fi
    done
}

101 102 103 104 105 106 107 108 109 110 111 112
list_stuff () {
    echo -n "$1 "
    if $pgml $1 > /dev/null 2>&1; then
        echo "ok"
    else
        echo "$pgm $1 FAIL"
        $pgm $1
        exit 1
    fi
}


MARCHE Claude's avatar
MARCHE Claude committed
113 114 115 116
echo "=== Checking drivers ==="
drivers drivers
echo ""

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
117
echo "=== Parsing good files  ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
118
goods bench/typing/bad --parse-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
119 120 121
echo ""

echo "=== Type-checking bad files ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
122
bads bench/typing/bad --type-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
123 124 125
echo ""

echo "=== Type-checking good files ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
126
goods bench/typing/good --type-only
MARCHE Claude's avatar
MARCHE Claude committed
127 128
goods examples --type-only
goods examples/tptp --type-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
129 130
echo ""

131 132
echo "=== Type-checking theories ==="
goods theories --type-only
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
133 134
echo ""

135 136 137
echo "=== Parsing programs ==="
pgml_options=--parse-only
programs bench/programs/bad-typing
138
programs bench/programs/good
139 140 141 142 143 144 145 146
programs examples/programs
echo ""

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

147 148 149 150 151
echo "=== Type-checking modules ==="
pgml_options=--type-only
programs modules
echo ""

152 153
echo "=== Type-checking good programs ==="
pgml_options=--type-only
154
programs bench/programs/good
155 156 157
programs examples/programs
echo ""

158 159 160
echo "=== VC generation on good programs ==="
pgml_options=
programs bench/programs/good
161
programs examples/programs
MARCHE Claude's avatar
MARCHE Claude committed
162
programs examples/programs/vacid_0_binary_heaps "-I examples/programs/vacid_0_binary_heaps"
163
echo ""
164

165 166 167 168
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""

169 170 171 172 173 174 175 176
echo "=== Checking --list-* ==="
list_stuff --list-transforms
list_stuff --list-printers
list_stuff --list-provers
list_stuff --list-formats
list_stuff --list-metas
list_stuff --list-debug-flags
echo ""