2017-05-17 02:34:15 +00:00
|
|
|
#!/bin/bash
|
|
|
|
|
2018-07-18 04:16:42 +00:00
|
|
|
ERROUTPUT=/tmp/orca-rez-err.$$
|
2017-05-17 02:34:15 +00:00
|
|
|
|
|
|
|
FILENAME="$1"
|
|
|
|
shift
|
|
|
|
|
2019-07-15 04:28:25 +00:00
|
|
|
DESTBASENAME="$1"
|
|
|
|
shift
|
|
|
|
|
2017-05-17 02:34:15 +00:00
|
|
|
if echo $FILENAME | grep -v '\.rez$' > /dev/null
|
|
|
|
then
|
|
|
|
echo Expected first argument to be a *.rez file but got $FILENAME
|
|
|
|
exit 1
|
|
|
|
fi
|
|
|
|
|
2019-07-15 04:28:25 +00:00
|
|
|
SRCBASENAME=`echo $FILENAME | sed 's/\.rez$//'`
|
|
|
|
SRCOBJNAME="${SRCBASENAME}.r"
|
2017-05-17 02:34:15 +00:00
|
|
|
|
2019-07-15 04:28:25 +00:00
|
|
|
DESTDEPSNAME="${DESTBASENAME}.rez.d"
|
|
|
|
DESTOBJNAME="${DESTBASENAME}.r"
|
|
|
|
|
|
|
|
$ORCA --trace-gsos compile "$@" keep="${SRCOBJNAME}" "$FILENAME" 2> $ERROUTPUT
|
2017-05-17 02:34:15 +00:00
|
|
|
RESULT=$?
|
|
|
|
|
2018-07-18 04:16:42 +00:00
|
|
|
awk '
|
|
|
|
/^[A-Za-z][A-Za-z]*\(.*\)$/ {
|
|
|
|
next
|
|
|
|
}
|
|
|
|
|
|
|
|
{
|
|
|
|
print
|
|
|
|
}
|
|
|
|
|
|
|
|
/^File [^ ]*; Line [0-9][0-9]*;/ {
|
|
|
|
sub(/;/,"",$4)
|
|
|
|
LINENO=$4
|
|
|
|
sub(/^File [^ ]*; Line [0-9][0-9]*/, "", $0)
|
2019-07-19 15:51:55 +00:00
|
|
|
printf("%s/%s:%d:0: error: %s\n", PWD, FILE, LINENO, $0)
|
2018-07-18 04:16:42 +00:00
|
|
|
}
|
|
|
|
' "PWD=`pwd`" "FILE=$FILENAME" $ERROUTPUT >&2
|
2017-05-17 02:34:15 +00:00
|
|
|
|
|
|
|
if [ "$RESULT" -ne 0 ]
|
|
|
|
then
|
2018-07-18 04:16:42 +00:00
|
|
|
rm -f $ERROUTPUT
|
2019-07-15 04:28:25 +00:00
|
|
|
rm -f $SRCOBJNAME
|
2017-05-17 02:34:15 +00:00
|
|
|
exit $RESULT
|
|
|
|
fi
|
|
|
|
|
2019-07-15 04:28:25 +00:00
|
|
|
mkdir -p `dirname "$DESTOBJNAME"`
|
|
|
|
mv -f "$SRCOBJNAME" "$DESTOBJNAME" 2> /dev/null
|
|
|
|
|
2017-05-17 02:34:15 +00:00
|
|
|
DEPS=`awk '
|
|
|
|
/^FastFileLoad/ {
|
|
|
|
sub(/^FastFileLoad\(/, "");
|
|
|
|
sub(/\)$/, "");
|
2018-07-18 04:16:42 +00:00
|
|
|
print}' $ERROUTPUT | sort -u | while read FILE
|
2017-05-17 02:34:15 +00:00
|
|
|
do
|
|
|
|
if [ -f "$FILE" ]
|
|
|
|
then
|
|
|
|
echo $FILE
|
|
|
|
fi
|
|
|
|
done`
|
|
|
|
|
2019-07-15 04:28:25 +00:00
|
|
|
echo $DESTOBJNAME: $DEPS > $DESTDEPSNAME
|
2018-07-18 04:16:42 +00:00
|
|
|
rm -f $ERROUTPUT
|
2017-05-17 02:34:15 +00:00
|
|
|
|
|
|
|
exit 0
|