bench 2.03 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
}

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
79 80
# 1. Syntax
echo "=== Parsing good files  ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
81
goods bench/typing/bad --parse-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
82 83 84 85
echo ""

# 2. Typing
echo "=== Type-checking bad files ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
86
bads bench/typing/bad --type-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
87 88 89
echo ""

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

93 94
echo "=== Type-checking theories ==="
goods theories --type-only
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
95 96
echo ""

97
echo "=== Checking drivers ==="
98
drivers drivers
Francois Bobot's avatar
Francois Bobot committed
99 100
echo ""

101 102 103 104 105 106 107 108 109 110 111 112 113
echo "=== Parsing programs ==="
pgml_options=--parse-only
programs bench/programs/bad-typing
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
114
programs bench/programs/good
115 116 117
programs examples/programs
echo ""