Revision c518d082
Added by Xavier Thirioux almost 8 years ago
| test/test-compile.sh | ||
|---|---|---|
| 51 | 51 |
fi |
| 52 | 52 |
fi |
| 53 | 53 |
popd > /dev/null |
| 54 |
echo "lustrec ($rlustrec1), gcc($rgcc1), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
|
|
| 54 |
echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
|
|
| 55 | 55 |
done < $file_list |
| 56 | 56 |
} |
| 57 | 57 |
|
| ... | ... | |
| 78 | 78 |
else |
| 79 | 79 |
rgcc2="VALID" |
| 80 | 80 |
fi |
| 81 |
echo "lustrec inlined ($rlustrec2), gcc ($rgcc2),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
|
|
| 81 |
echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
|
|
| 82 | 82 |
popd > /dev/null |
| 83 | 83 |
done < $file_list |
| 84 | 84 |
} |
| ... | ... | |
| 106 | 106 |
fi |
| 107 | 107 |
# Cheching witness |
| 108 | 108 |
pushd $build > /dev/null |
| 109 |
lustrec -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 2>/dev/null
|
|
| 109 |
$LUSTREC -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 2>/dev/null
|
|
| 110 | 110 |
popd > /dev/null |
| 111 | 111 |
z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
|
| 112 | 112 |
if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then |
| ... | ... | |
| 119 | 119 |
rinlining="INVALID" |
| 120 | 120 |
exit 1 |
| 121 | 121 |
fi |
| 122 |
echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
|
|
| 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"
|
|
| 123 | 123 |
popd > /dev/null |
| 124 | 124 |
done < $file_list |
| 125 | 125 |
|
| ... | ... | |
| 146 | 146 |
else |
| 147 | 147 |
rhorn="VALID" |
| 148 | 148 |
fi |
| 149 |
echo "horn-pdr ($rhorn), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
|
|
| 149 |
echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
|
|
| 150 | 150 |
popd > /dev/null |
| 151 | 151 |
done < $file_list |
| 152 | 152 |
} |
Also available in: Unified diff
- added generation of clock information in interface (.lusi) files
- added clock checking between interface and implementation files