bench 2.53 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
# Useless in this script ?
# export WHY3LIB=lib
# export WHY3DATA=.
Andrei Paskevich's avatar
Andrei Paskevich committed
8
# export WHY3LOADPATH=theories
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
9 10

pgm=$1
Andrei Paskevich's avatar
Andrei Paskevich committed
11

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
12
goods () {
Andrei Paskevich's avatar
Andrei Paskevich committed
13 14
    for f in $1/*.[wm][hl][yw] ; do
	echo -n "  $f... "
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
15 16
	# running Why
	if ! $pgm $2 $f > /dev/null 2>&1; then
Andrei Paskevich's avatar
Andrei Paskevich committed
17 18
	    echo "FAILED!"
#            echo "env: WHY3DATA='$WHY3DATA'"
19 20
            echo "invocation: $pgm $2 $f"
            echo "result:"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
21 22 23
	    $pgm $2 $f
	    exit 1
	fi
Andrei Paskevich's avatar
Andrei Paskevich committed
24
	echo "ok"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
25 26 27 28
    done
}

bads () {
Andrei Paskevich's avatar
Andrei Paskevich committed
29 30
    for f in $1/*.[wm][hl][yw] ; do
	echo -n "  $f... "
31
	if $pgm $2 $f > /dev/null 2>&1; then
Andrei Paskevich's avatar
Andrei Paskevich committed
32 33 34
	    echo "SHOULD FAIL!"
#            echo "env: WHY3DATA='$WHY3DATA'"
            echo "invocation: $pgm $2 $f"
35
	    exit 1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
36
	fi
Andrei Paskevich's avatar
Andrei Paskevich committed
37
	echo "ok"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
38 39 40
    done
}

Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
41 42
drivers () {
    for f in $1/*.drv; do
43
        if [ $f = "drivers/ocaml.drv" ]; then continue; fi
Andrei Paskevich's avatar
Andrei Paskevich committed
44
	echo -n "  $f... "
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
45
	# running Why
46
	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
47
	    echo "why FAILED"
48
            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
49 50
	    exit 1
	fi
Andrei Paskevich's avatar
Andrei Paskevich committed
51
	echo "ok"
52 53 54
    done
}

55 56 57
valid_goals () {
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
Andrei Paskevich's avatar
Andrei Paskevich committed
58
	if $pgm -t 10 -P alt-ergo $f | grep -q -v Valid; then
59
	    echo "valid test $f failed!"
Andrei Paskevich's avatar
Andrei Paskevich committed
60 61
	    echo "$pgm -P alt-ergo $f"
	    $pgm -t 10 -P alt-ergo $f
62
	    exit 1
63
       else
64
	    echo "ok"
Andrei Paskevich's avatar
Andrei Paskevich committed
65
       fi
66 67 68
    done
}

69 70
list_stuff () {
    echo -n "$1 "
Andrei Paskevich's avatar
Andrei Paskevich committed
71
    if $pgm $1 > /dev/null 2>&1; then
72 73 74 75 76 77 78 79 80
        echo "ok"
    else
        echo "$pgm $1 FAIL"
        $pgm $1
        exit 1
    fi
}


81 82
echo "=== Checking theories ==="
goods theories
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
83 84
echo ""

85 86
echo "=== Checking modules ==="
goods modules
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
87 88
echo ""

89 90
echo "=== Checking bad files ==="
goods bench/typing/bad --parse-only
Andrei Paskevich's avatar
Andrei Paskevich committed
91
goods bench/programs/bad-typing --parse-only
92
bads bench/typing/bad --type-only
Andrei Paskevich's avatar
Andrei Paskevich committed
93
bads bench/programs/bad-typing --type-only
94 95
echo ""

96 97
echo "=== Checking good files ==="
goods bench/typing/good
Andrei Paskevich's avatar
Andrei Paskevich committed
98
goods bench/programs/good
99 100 101 102 103
goods examples/bts
goods examples/tests
goods examples/tests-provers
goods examples/check-builtin
goods examples/logic
Andrei Paskevich's avatar
Andrei Paskevich committed
104 105 106 107
goods examples
goods examples/foveoos11-cm
goods examples/hoare_logic
goods examples/vacid_0_binary_heaps "-I examples/vacid_0_binary_heaps"
108 109 110 111 112 113
goods examples/bitvectors "-I examples/bitvectors"
goods examples/in_progress
echo ""

echo "=== Checking drivers ==="
drivers drivers
114
echo ""
115

116 117 118 119
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""

120 121 122 123 124 125 126 127
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 ""