This type really should just be a regular int as no usages rely on it's
32 bitness (it's only meaningful as a bit position and not a bit mask).
This also fixes a printf which uses the variable with a regular %d.
Signed-off-by: Peter Crosthwaite <peter.crosthwaite@xilinx.com>
Reviewed-by: Peter Maydell <peter.maydell@linaro.org>
Message-id: 2a99d31f377aee371476d9da8fd0d1b7efa30f63.1393372019.git.peter.crosthwaite@xilinx.com
Signed-off-by: Peter Maydell <peter.maydell@linaro.org>
024c6e2ea5