Skip to content

Commit

Permalink
aarch64/vspace: avoid unnecessary casts
Browse files Browse the repository at this point in the history
Type invLabel consistently as word_t, not sometimes as unsigned int.
This makes verification easier because it avoids unnecessary casts.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
  • Loading branch information
lsf37 committed Jan 16, 2024
1 parent 2b29446 commit 0398d34
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions src/arch/arm/64/kernel/vspace.c
Original file line number Diff line number Diff line change
Expand Up @@ -1073,7 +1073,7 @@ void deleteASIDPool(asid_t asid_base, asid_pool_t *pool)
}
}

static void doFlush(int invLabel, vptr_t start, vptr_t end, paddr_t pstart)
static void doFlush(word_t invLabel, vptr_t start, vptr_t end, paddr_t pstart)
{
switch (invLabel) {
case ARMVSpaceClean_Data:
Expand Down Expand Up @@ -1110,7 +1110,7 @@ static void doFlush(int invLabel, vptr_t start, vptr_t end, paddr_t pstart)

/* ================= INVOCATION HANDLING STARTS HERE ================== */

static exception_t performVSpaceFlush(int invLabel, vspace_root_t *vspaceRoot, asid_t asid,
static exception_t performVSpaceFlush(word_t invLabel, vspace_root_t *vspaceRoot, asid_t asid,
vptr_t start, vptr_t end, paddr_t pstart)
{

Expand Down Expand Up @@ -1195,7 +1195,7 @@ static exception_t performPageInvocationUnmap(cap_t cap, cte_t *ctSlot)
return EXCEPTION_NONE;
}

static exception_t performPageFlush(int invLabel, vspace_root_t *vspaceRoot, asid_t asid,
static exception_t performPageFlush(word_t invLabel, vspace_root_t *vspaceRoot, asid_t asid,
vptr_t start, vptr_t end, paddr_t pstart)
{
if (config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) {
Expand Down

0 comments on commit 0398d34

Please sign in to comment.