faultline=`echo "$faultline" | sed -e 's/\[/\\\[/g; s/\]/\\\]/g'`
cat $T.oo | sed -e "s/\($faultline\)/\*\1 <-- trapping instruction/g"
faultline=`echo "$faultline" | sed -e 's/\[/\\\[/g; s/\]/\\\]/g'`
cat $T.oo | sed -e "s/\($faultline\)/\*\1 <-- trapping instruction/g"