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
|
#!/bin/bash
pgm="bin/why3 prove"
coma_bad () {
test -d $1 || exit 1
for f in $1/*.coma ; do
printf " $f... "
if $pgm $2 $f > /dev/null 2>&1; then
echo "failed! (should have an error)"
echo $pgm $2 $f
$pgm $2 $f
exit 1
fi
echo "ok"
done
}
coma_good () {
test -d $1 || exit 1
rm -f bench_errors
rm -f bench_error
for f in $1/*.$2 ; do
printf " $f... "
if ! $pgm $f > /dev/null 2> bench_error; then
echo "failed!"
echo "invocation: $pgm $opts $f" | tee -a bench_errors
cat bench_error | tee -a bench_errors
rm -f bench_errors bench_error
exit 1
fi
rm -f bench_error
echo "ok"
done
}
simple_test() {
if ! "$@" > /dev/null 2> /dev/null; then
echo "failed!"
echo "$@"
"$@"
exit 1
fi
echo "ok"
}
replay () {
pgm="bin/why3 replay"
test -d $1 || exit 1
for f in $1/*/; do
printf " $f... "
simple_test $pgm $f
done
}
make -j
echo "=== Checking bad files (Coma) ==="
coma_bad ./bench/plugins/coma/bad
echo ""
echo "=== Checking good files (Coma) ==="
coma_good ./examples/coma coma
coma_good ./bench/plugins/coma/good coma
echo ""
echo "=== Checking replay (Coma) ==="
replay ./examples/coma
echo ""
|
