The beri boot loaders depend on symbols defined in linker scripts or
assembly files. The boot loaders do not care about the type of these
symbols but just want to extract a pointer to them. Older versions of
GCC permitted external symbols to be declared of type 'void' and then
'&foo' generated a void pointer to the memory at the symbol's address.
However, void objects are not valid C and newer versions of GCC error if
these are used. Instead, declare these symbols as being bytes (or
an array of bytes in the cheri_sdcard_vaddr case).
Sponsored by: DARPA / AFRL