Revision c518d082
Added by Xavier Thirioux almost 9 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