aarch64/vspace: adjust type for verification

Bring the type of `i` into line with what the other architectures do
in this function. This makes it easier to re-use those proofs.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein
2024-01-18 17:18:02 +11:00
parent 0398d34ad0
commit 95cfd473e6

View File

@@ -1649,7 +1649,7 @@ exception_t decodeARMMMUInvocation(word_t invLabel, word_t length, cptr_t cptr,
return decodeARMFrameInvocation(invLabel, length, cte, cap, call, buffer);
case cap_asid_control_cap: {
unsigned int i;
word_t i;
asid_t asid_base;
word_t index, depth;
cap_t untyped, root;