libvixl: Fix format strings for several int64_t values

"%d" or "%x" won't work on hosts where int values are smaller than 64 bit.

Signed-off-by: Stefan Weil <sw@weilnetz.de>
Message-id: 1394219753-26106-1-git-send-email-sw@weilnetz.de
Signed-off-by: Peter Maydell <peter.maydell@linaro.org>