# CONFIG_VMI is not set
