Extend objdump's --show-all-symbols option so that it also shows the extra symbols...