# CONFIG_HVC_OLD_HVSI is not set