1
2
3
4
5
6
7
8
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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
|
#!/bin/sh -eu
# regression tests for why3
REPLAYOPT=""
REGTESTS_MODE=""
while test $# != 0; do
case "$1" in
"--force")
REPLAYOPT="$REPLAYOPT --force"
;;
"--obsolete-only")
REPLAYOPT="$REPLAYOPT --obsolete-only"
;;
"--ignore-shapes")
REPLAYOPT="$REPLAYOPT --ignore-shapes"
;;
"--prover")
REPLAYOPT="$REPLAYOPT --prover $2"
shift
;;
"--reduced-mode")
REGTESTS_MODE="REDUCED"
;;
*)
echo "$0: Unknown option '$1'"
exit 2
esac
shift
done
TMP=$PWD/why3regtests.out
TMPERR=$PWD/why3regtests.err
# Current directory is /examples
cd `dirname $0`
# too early to do that
# REPLAYOPT="$REPLAYOPT --smoke-detector top"
res=0
export success=0
export total=0
export sessions=""
export shapes=""
run_dir () {
if [ "$REGTESTS_MODE" = "REDUCED" ]; then
if [ -f $1/reduced_regtests.list ]; then
LIST=`sed $1/reduced_regtests.list -n -e "s&^\([^ #]\+\).*&$1/\1/why3session.xml&p"`
else
LIST=
fi
else
LIST=`ls $1/*/why3session.xml`
fi
for f in $LIST; do
d=`dirname $f`
printf "Replaying $d ... "
if ../bin/why3.opt replay -q $REPLAYOPT $2 $d 2> $TMPERR > $TMP ; then
printf "OK"
cat $TMP $TMPERR
success=`expr $success + 1`
else
ret=$?
printf "FAILED (ret code=$ret):"
out=`head -1 $TMP`
if test -z "$out" ; then
echo "standard error: (standard output empty)"
cat $TMPERR
else
cat $TMP
fi
res=1
fi
total=`expr $total + 1`
done
sessions="$sessions $1/*/why3session.xml"
shapes="$shapes $1/*/why3shapes.gz"
}
echo "=== Examples and Case Studies === MUST REPLAY AND ALL GOALS PROVED ==="
echo ""
run_dir . ""
run_dir micro-c ""
run_dir python ""
run_dir double_wp "-L double_wp"
run_dir avl "-L avl"
run_dir c_cursor "-L c_cursor"
run_dir foveoos11-cm ""
run_dir vacid_0_binary_heaps "-L vacid_0_binary_heaps"
run_dir verifythis_2016_matrix_multiplication "-L verifythis_2016_matrix_multiplication"
run_dir WP_revisited ""
run_dir prover "-L prover --warn-off=unused_variable"
run_dir multiprecision "-L multiprecision"
run_dir c_cursor "-L c_cursor"
run_dir numeric ""
echo ""
echo "Score on Examples and Case Studies: $success/$total"
echo ""
echo "=== Standard Library ==="
echo ""
run_dir stdlib ""
echo ""
echo "=== Tests ==="
echo ""
# there's no session there...
# run_dir tests
run_dir tests-provers ""
echo ""
echo "=== Check Builtin translation ==="
echo ""
run_dir check-builtin ""
echo ""
echo "=== BTS ==="
echo ""
run_dir bts ""
echo ""
echo "=== Logic ==="
echo ""
run_dir logic ""
run_dir bitvectors "-L bitvectors"
echo ""
echo "=== MLCFG ==="
echo ""
run_dir mlcfg ""
echo ""
echo "Summary : $success/$total"
echo "Sessions size : "`wc -cl $sessions | tail -1`
echo "Shapes size : "`wc -cl $shapes | tail -1`
exit $res
|
