|
1
|
#!/bin/bash
|
|
2
|
|
|
3
|
#eval set -- $(getopt -n $0 "-aciwvh:" -- "$@")
|
|
4
|
|
|
5
|
declare c i w h a v r
|
|
6
|
declare -a files
|
|
7
|
|
|
8
|
#SRC_PREFIX="../.."
|
|
9
|
#SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
|
|
10
|
NOW=`date "+%y-%m-%d-%H:%M"`
|
|
11
|
report=`pwd`/horn-report-$NOW
|
|
12
|
#LUSTREC="../../_build/src/lustrec"
|
|
13
|
LUSTREC=../bin/lustrec
|
|
14
|
mkdir -p build-$NOW
|
|
15
|
build=`pwd`/build-$NOW
|
|
16
|
|
|
17
|
|
|
18
|
check_horn () {
|
|
19
|
while IFS=, read -r file main opts
|
|
20
|
do
|
|
21
|
name=`basename "$file" .lus`
|
|
22
|
if [ "$name" = "$file" ]; then
|
|
23
|
return 0
|
|
24
|
fi
|
|
25
|
dir=${SRC_PREFIX}`dirname "$file"`
|
|
26
|
pushd $dir > /dev/null
|
|
27
|
|
|
28
|
# Checking horn backend
|
|
29
|
if [ "$main" != "" ]; then
|
|
30
|
$LUSTREC -horn-traces -horn-query -d $build -verbose 0 $opts -node $main "$name".lus
|
|
31
|
else
|
|
32
|
$LUSTREC -horn-traces -horn-query -d $build -verbose 0 $opts "$name".lus
|
|
33
|
fi
|
|
34
|
if [ $? -ne 0 ]; then
|
|
35
|
rlustrec="ERROR";
|
|
36
|
else
|
|
37
|
rlustrec="OK"
|
|
38
|
fi
|
|
39
|
if [ $verbose -gt 0 ]; then
|
|
40
|
echo "lustrec ($rlustrec), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
|
|
41
|
else
|
|
42
|
echo "lustrec ($rlustrec), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
|
|
43
|
fi
|
|
44
|
popd > /dev/null
|
|
45
|
done < $file_list
|
|
46
|
}
|
|
47
|
|
|
48
|
usage () {
|
|
49
|
echo "usage: $0 [-aciwh] file_list"
|
|
50
|
echo "-r: regression test for horn backend"
|
|
51
|
echo "-v <int>: verbose level"
|
|
52
|
}
|
|
53
|
|
|
54
|
verbose=0
|
|
55
|
nobehavior=1
|
|
56
|
|
|
57
|
while [ $# -gt 0 ] ; do
|
|
58
|
case "$1" in
|
|
59
|
-v) shift ; verbose="$1"; shift ;;
|
|
60
|
-r) nobehavior=0; r=1 ; shift ;;
|
|
61
|
--) shift ;;
|
|
62
|
-*) echo "bad option '$1'" ; exit 1 ;;
|
|
63
|
*) files=("${files[@]}" "$1") ; shift ;;
|
|
64
|
esac
|
|
65
|
done
|
|
66
|
|
|
67
|
file_list=${files[0]}
|
|
68
|
|
|
69
|
|
|
70
|
if [ ${#files} -eq 0 ] ; then
|
|
71
|
echo input list required
|
|
72
|
usage
|
|
73
|
exit 1
|
|
74
|
fi
|
|
75
|
|
|
76
|
[ ! -z "$r" ] && check_horn
|
|
77
|
mv $report $build
|
|
78
|
[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage
|
|
79
|
echo "DONE"
|