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
|
#!/bin/bash
dir=`dirname $0`
updateoracle=false
files=""
success=true
while test $# != 0; do
case "$1" in
"-update-oracle")
updateoracle=true;;
"-"*)
printf "unknown option: %s\n" "$1"
printf "usage: ide-bench [-update-oracle] <files>\n"
printf " <files> must be given with the '.mlw' suffix\n"
printf " if <files> empty, use all files from directory 'ide'\n"
exit 2;;
*)
files="$files $1"
esac
shift
done
if test "$files" = "" ; then
files="$dir/ide/*.mlw"
fi
# $1 = dir, $2 = filename
run () {
printf "$2..."
file_path="$1/$2"
oracle_file="$1/oracles/$2.oracle"
echo "$file_path"
xvfb-run -a bin/why3.opt ide --batch="down;down;type split_vc;wait 1;down;down;color;" "${file_path}.mlw" > "${file_path}.out"
str_oracle=$(tr -d ' \n' < "${oracle_file}")
str_out=$(tr -d ' \n' < "${file_path}.out")
if [ "$str_oracle" = "$str_out" ] ; then
echo "ok"
else
if $updateoracle; then
echo "Updating oracle for ${file_path}"
mv "${file_path}.out" "${oracle_file}"
else
echo "FAILED!"
echo "Oracle is ${str_oracle}"
echo "Output is ${str_out}"
echo "diff is the following:"
echo "${file_path}"
diff "${oracle_file}" "${file_path}.out"
success=false
fi
fi
}
for file in $files; do
filedir=`dirname $file`
filebase=`basename $file .mlw`
run $filedir $filebase
done
if $success; then
exit 0
else
exit 1
fi
|
