bench 2.32 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2 3 4 5 6 7
#!/bin/sh

# auto bench for why

export WHYLIB=../lib

pgm=$1
8
pgml=$2
9
pgml_options=
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37

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"
	    $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
38 39 40 41
drivers () {
    for f in $1/*.drv; do
	echo -n "  "$f"... "
	# running Why
42
	if ! echo "theory Test goal G : 1=2 end" | $pgm --driver $f - > /dev/null 2>&1; then
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
43
	    echo "why FAILED"
44
            echo "theory Test goal G : 1=2 end" | $pgm --driver $f -
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
45 46 47 48 49 50
	    exit 1
	fi
	echo "why ok... "
    done
}

51 52 53
programs () {
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
54 55 56
	if ! $pgml $pgml_options $f > /dev/null 2>&1; then 
	    echo 
	    echo "$pgml $pgml_options $f"
57 58 59 60 61 62 63 64
	    echo "FAILED!"
	    exit 1 
        else 
	    echo "ok"
	fi
    done
}

65 66 67 68 69 70 71 72 73 74 75 76 77 78
bad_programs () {
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
	if $pgml $pgml_options $f > /dev/null 2>&1; then 
	    echo 
	    echo "$pgml $pgml_options $f"
	    echo "SHOULD FAIL!"
	    exit 1 
        else 
	    echo "ok"
	fi
    done
}

79 80 81 82 83 84 85 86 87 88 89 90
valid_goals () {
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
	if $pgml -P alt-ergo $f | grep -q -v Valid; then
	    echo "valid test $f failed!"
	    exit 1
       else 
	    echo "ok"
	fi
    done
}

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
91 92
# 1. Syntax
echo "=== Parsing good files  ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
93
goods bench/typing/bad --parse-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94 95 96 97
echo ""

# 2. Typing
echo "=== Type-checking bad files ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
98
bads bench/typing/bad --type-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
99 100 101
echo ""

echo "=== Type-checking good files ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
102
goods bench/typing/good --type-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
103 104
echo ""

105 106
echo "=== Type-checking theories ==="
goods theories --type-only
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
107 108
echo ""

109 110 111
echo "=== Parsing programs ==="
pgml_options=--parse-only
programs bench/programs/bad-typing
112
programs bench/programs/good
113 114 115 116 117 118 119 120 121 122
programs examples/programs
echo ""

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

echo "=== Type-checking good programs ==="
pgml_options=--type-only
123
programs bench/programs/good
124 125 126
programs examples/programs
echo ""

127 128 129 130
echo "=== Checking drivers ==="
drivers drivers
echo ""

131 132 133 134 135
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""