Revision 7291cb80
Added by Xavier Thirioux over 9 years ago
| test/test-compile.sh | ||
|---|---|---|
| 4 | 4 |
#LUSTREC="../../_build/src/lustrec" |
| 5 | 5 |
LUSTREC=lustrec |
| 6 | 6 |
mkdir -p build |
| 7 |
cd build |
|
| 8 |
|
|
| 7 |
build=`pwd`"/build" |
|
| 9 | 8 |
while IFS=, read -r file main opts |
| 10 | 9 |
do |
| 11 | 10 |
echo fichier:$file |
| 12 | 11 |
# echo main:$main |
| 13 |
# echo opts:$opts
|
|
| 12 |
# echo opts:$opts
|
|
| 14 | 13 |
rm -f witness* |
| 14 |
name=`basename "$file" .lus` |
|
| 15 |
dir=`dirname "$file"` |
|
| 16 |
pushd $dir > /dev/null |
|
| 15 | 17 |
if [ "$main" != "" ]; then |
| 16 |
$LUSTREC -d build -verbose 0 $opts -node $main ../$file;
|
|
| 18 |
$LUSTREC -d $build -verbose 0 $opts -node $main "$name".lus;
|
|
| 17 | 19 |
if [ $? -ne 0 ]; then |
| 18 | 20 |
rlustrec1="INVALID"; |
| 19 | 21 |
else |
| 20 | 22 |
rlustrec1="VALID" |
| 21 | 23 |
fi |
| 22 |
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null |
|
| 24 |
pushd $build > /dev/null |
|
| 25 |
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null |
|
| 26 |
popd > /dev/null |
|
| 23 | 27 |
if [ $? -ne 0 ]; then |
| 24 | 28 |
rgcc1="INVALID"; |
| 25 | 29 |
else |
| 26 | 30 |
rgcc1="VALID" |
| 27 | 31 |
fi |
| 28 | 32 |
# Removing Generated lusi file |
| 29 |
grep generated ../${file}i > /dev/null
|
|
| 30 |
if [ $? -ne 1 ];then |
|
| 31 |
rm ../${file}i
|
|
| 32 |
fi |
|
| 33 |
#grep generated ../${file}i > /dev/null
|
|
| 34 |
#if [ $? -ne 1 ];then
|
|
| 35 |
# rm ../${file}i
|
|
| 36 |
#fi
|
|
| 33 | 37 |
# Checking inlining |
| 34 |
$LUSTREC -d build -verbose 0 $opts -inline -witnesses -node $main ../$file;
|
|
| 38 |
$LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
|
|
| 35 | 39 |
if [ $? -ne 0 ]; then |
| 36 | 40 |
rlustrec2="INVALID"; |
| 37 | 41 |
else |
| 38 | 42 |
rlustrec2="VALID" |
| 39 | 43 |
fi |
| 40 |
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null |
|
| 44 |
pushd $build > /dev/null |
|
| 45 |
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null |
|
| 46 |
popd > /dev/null |
|
| 41 | 47 |
if [ $? -ne 0 ]; then |
| 42 | 48 |
rgcc2="INVALID"; |
| 43 | 49 |
else |
| 44 | 50 |
rgcc2="VALID" |
| 45 | 51 |
fi |
| 46 | 52 |
# Cheching witness |
| 53 |
pushd $build > /dev/null |
|
| 47 | 54 |
lustreh -horn -node check witness.lus 2>/dev/null |
| 55 |
popd > /dev/null |
|
| 48 | 56 |
z3="`z3 -t:10 witness.smt2 | xargs`" |
| 49 | 57 |
if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then |
| 50 | 58 |
rinlining="VALID"; |
| ... | ... | |
| 57 | 65 |
exit 1 |
| 58 | 66 |
fi |
| 59 | 67 |
# Checking horn backend |
| 60 |
$LUSTREC -horn -d build -verbose 0 $opts -node $main ../$file;
|
|
| 61 |
echo z3 `basename $file .lus`.smt2 | grep unsat
|
|
| 68 |
$LUSTREC -horn -d $build -verbose 0 $opts -node $main "$name".lus;
|
|
| 69 |
echo z3 "$name".smt2 | grep unsat
|
|
| 62 | 70 |
# TODO: This part of the script has to be optimized |
| 63 |
z3 -t:10 `basename $file .lus`.smt2 | grep unsat > /dev/null
|
|
| 71 |
z3 -t:10 "$name".smt2 | grep unsat > /dev/null
|
|
| 64 | 72 |
if [ $? -ne 0 ]; then |
| 65 | 73 |
rhorn="INVALID"; |
| 66 | 74 |
else |
| ... | ... | |
| 68 | 76 |
fi |
| 69 | 77 |
echo "lustrec ($rlustrec1),gcc($rgcc1),lustrec inline ($rlustrec2), gcc inline ($rgcc2), inlining valid ($rinlining),horn ($rhorn),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN" |
| 70 | 78 |
else |
| 71 |
$LUSTREC -d build -verbose 0 $opts ../$file;
|
|
| 79 |
$LUSTREC -d $build -verbose 0 $opts "$name".lus;
|
|
| 72 | 80 |
if [ $? -ne 0 ]; then |
| 73 | 81 |
rlustrec1="INVALID"; |
| 74 | 82 |
else |
| 75 | 83 |
rlustrec1="VALID" |
| 76 | 84 |
fi |
| 77 |
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null |
|
| 85 |
pushd $build > /dev/null |
|
| 86 |
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null |
|
| 87 |
popd > /dev/null |
|
| 78 | 88 |
if [ $? -ne 0 ]; then |
| 79 | 89 |
rgcc1="INVALID"; |
| 80 | 90 |
else |
| 81 | 91 |
rgcc1="VALID" |
| 82 | 92 |
fi |
| 83 |
$LUSTREC -horn -d build -verbose 0 $opts ../$file |
|
| 93 |
$LUSTREC -horn -d $build -verbose 0 $opts ../$file
|
|
| 84 | 94 |
echo "lustrec ($rlustrec1), gcc($rgcc1), horn($rhorn), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN" |
| 85 | 95 |
fi |
| 86 |
done < ../tests_ok.list |
|
| 96 |
popd > /dev/null |
|
| 97 |
done < tests_ok.list |
|
Also available in: Unified diff
- merged test script
- added -d support
- corrected #open parser problem
- corrected interface/implementation (.lusi/.lus) checking
for types (not yet for clocks)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@171 041b043f-8d7c-46b2-b46e-ef0dd855326e