e6a33e45c2
sipi_vector is an int; it is shifted by 12 and passed as a 64-bit value, which makes Coverity think that we wanted (uint64_t)sipi_vector << 12. But actually it must be between 0 and 255. Make this explicit. Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>