/* XXX Use device_printf, with a device. */