Did you guys ever look into the sparse address space annotations? We use them pretty successfully in the Linux kernel for little/big endian datatypes and pointers to userspace or I/O memory. The downside is that you need to add sparse to the build as a typechecker, the upside is that it's really easy and can be done gradually.