bench 1.44 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
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
9 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

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
63 64
# 1. Syntax
echo "=== Parsing good files  ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
65
goods bench/typing/bad --parse-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
66 67 68 69
echo ""

# 2. Typing
echo "=== Type-checking bad files ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
70
bads bench/typing/bad --type-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
71 72 73
echo ""

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

77 78
echo "=== Type-checking theories ==="
goods theories --type-only
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
79 80
echo ""

81
echo "=== Checking drivers ==="
82
drivers drivers
Francois Bobot's avatar
Francois Bobot committed
83 84
echo ""

85 86 87 88
echo "=== Type-checking programs ==="
programs examples/programs
echo ""