Fix two cases where device_printf() was used with an empty format.