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