Revision 1699b8ff
Added by Pierre-Loïc Garoche over 10 years ago
test/test-compile.sh | ||
---|---|---|
1 | 1 |
#!/bin/bash |
2 | 2 |
|
3 |
eval set -- $(getopt -n $0 -o "-ciwh:" -- "$@")
|
|
3 |
eval set -- $(getopt -n $0 -o "-aciwvh:" -- "$@")
|
|
4 | 4 |
|
5 |
declare c i w h |
|
5 |
declare c i w h a v
|
|
6 | 6 |
declare -a files |
7 | 7 |
|
8 |
SRC_PREFIX=`svn info | grep Working | sed "s/.*: //"`/lustre_compiler |
|
8 | 9 |
NOW=`date "+%y%m%d%H%M"` |
9 | 10 |
report=`pwd`/report-$NOW |
10 | 11 |
#LUSTREC="../../_build/src/lustrec" |
... | ... | |
17 | 18 |
while IFS=, read -r file main opts |
18 | 19 |
do |
19 | 20 |
name=`basename "$file" .lus` |
20 |
dir=`dirname "$file"` |
|
21 |
dir=${SRC_PREFIX}/`dirname "$file"`
|
|
21 | 22 |
pushd $dir > /dev/null |
22 | 23 |
if [ "$main" != "" ]; then |
23 | 24 |
$LUSTREC -d $build -verbose 0 $opts -node $main "$name".lus; |
... | ... | |
51 | 52 |
fi |
52 | 53 |
fi |
53 | 54 |
popd > /dev/null |
54 |
echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN" |
|
55 |
if [ $verbose -gt 0 ]; then |
|
56 |
echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report; |
|
57 |
else |
|
58 |
echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN" |
|
59 |
fi; |
|
55 | 60 |
done < $file_list |
56 | 61 |
} |
57 | 62 |
|
... | ... | |
59 | 64 |
while IFS=, read -r file main opts |
60 | 65 |
do |
61 | 66 |
name=`basename "$file" .lus` |
62 |
dir=`dirname "$file"` |
|
67 |
dir=${SRC_PREFIX}/`dirname "$file"`
|
|
63 | 68 |
|
64 | 69 |
pushd $dir > /dev/null |
65 | 70 |
|
... | ... | |
78 | 83 |
else |
79 | 84 |
rgcc2="VALID" |
80 | 85 |
fi |
81 |
echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN" |
|
86 |
if [ $verbose -gt 0 ]; then |
|
87 |
echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report; |
|
88 |
else |
|
89 |
echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN" |
|
90 |
fi; |
|
82 | 91 |
popd > /dev/null |
83 | 92 |
done < $file_list |
84 | 93 |
} |
... | ... | |
88 | 97 |
while IFS=, read -r file main opts |
89 | 98 |
do |
90 | 99 |
name=`basename "$file" .lus` |
91 |
dir=`dirname "$file"` |
|
100 |
dir=${SRC_PREFIX}/`dirname "$file"`
|
|
92 | 101 |
pushd $dir > /dev/null |
93 | 102 |
$LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus; |
94 | 103 |
if [ $? -ne 0 ]; then |
... | ... | |
119 | 128 |
rinlining="INVALID" |
120 | 129 |
exit 1 |
121 | 130 |
fi |
122 |
echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN" |
|
131 |
if [ $verbose -gt 0 ]; then |
|
132 |
echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report; |
|
133 |
else |
|
134 |
echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN" |
|
135 |
fi |
|
123 | 136 |
popd > /dev/null |
124 | 137 |
done < $file_list |
125 | 138 |
|
... | ... | |
129 | 142 |
while IFS=, read -r file main opts |
130 | 143 |
do |
131 | 144 |
name=`basename "$file" .lus` |
132 |
dir=`dirname "$file"` |
|
145 |
dir=${SRC_PREFIX}/`dirname "$file"`
|
|
133 | 146 |
pushd $dir > /dev/null |
134 | 147 |
|
135 | 148 |
# Checking horn backend |
... | ... | |
146 | 159 |
else |
147 | 160 |
rhorn="VALID" |
148 | 161 |
fi |
149 |
echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN" |
|
162 |
if [ $verbose -gt 0 ]; then |
|
163 |
echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report; |
|
164 |
else |
|
165 |
echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN" |
|
166 |
fi |
|
150 | 167 |
popd > /dev/null |
151 | 168 |
done < $file_list |
152 | 169 |
} |
... | ... | |
158 | 175 |
echo "-i: compile with inline mode" |
159 | 176 |
echo "-w: compile with inline mode. Check the inlining with z3" |
160 | 177 |
echo "-h: check files with the horn-pdf backend (requires z3)" |
178 |
echo "-v <int>: verbose level" |
|
161 | 179 |
} |
162 | 180 |
|
181 |
verbose=0 |
|
163 | 182 |
nobehavior=1 |
164 | 183 |
|
165 | 184 |
while [ $# -gt 0 ] ; do |
Also available in: Unified diff
Updated test script: changed path and verbose mode