GDB has the concept of user registers which are numbered above the usual num_regs + num_pseudo_regs count. This can be used to deal with register names like "pc", "fp" and "sp" if these are not explicitly named in the ordinary registers.

"info reg sp" will print out the value of the stack pointer. This printing does not use the standard gdbarch_print_registers_info () function, but is done directly within registers_info () in infcmd.c.

The problem is if I try to print multiple user registers. For example "info reg sp fp" will print

sp fp: <the value of sp>
fp: <the value of fp>

I.e. the remainder of the string of register names is printed each time, rather than just the register concerned.

The problem is within registers_info (), where the name of the register is printed using

	printf_filtered ("%s: ", start);

either start needs to be temporarily terminated with a NULL at *end (is this string always mutable though), or a clean copy needs to be taken, used and then disposed of.

I'll try to work out a patch, but logged here for the time being.