/* * XXX Not sure why this is here, but so it is in Linux... Also, not * sure what the right type is: Linux uses dma_addr_t, but I don't * think bus_addr_t is right here -- paddr_t sounds more appropriate. */