Fix indentation to make it clearer what the arguments to a printf call

Fix indentation to make it clearer what the arguments to a printf call
are.

To extract a 32-bit big-endian quantity from a particular address, use
EXTRACT_32BITS(), don't do pointer casting - casting a "char *" or
"unsigned char *" to point to a multi-byte quantity doesn't guarantee
the pointer can be dereferenced and give you the right answer (SPARC
traps on unaligned pointer accesses, some other processor types might
also trap, or might ignore the low bits of the pointer).