fputs_filtered (paddress (gdbarch, addr), outfile);
fprintf_filtered (outfile, " %s", msymbol->linkage_name ());
if (section)
fputs_filtered (paddress (gdbarch, addr), outfile);
fprintf_filtered (outfile, " %s", msymbol->linkage_name ());
if (section)