its_send_vmovi 1121 drivers/irqchip/irq-gic-v3-its.c its_send_vmovi(its_dev, event); its_send_vmovi 1306 drivers/irqchip/irq-gic-v3-its.c its_send_vmovi(its_dev, event);