Imagelibrary/seL4
1
0
Fork 1
mirror of https://github.com/seL4/seL4.git synced 2026-04-04 22:39:54 +00:00
Code Issues Packages Projects Releases Wiki Activity

aarch64/vspace: avoid unnecessary casts

Browse Source 
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>
This commit is contained in:
Gerwin Klein
2024-01-11 12:53:37 +11:00
parent 2b29446484
commit 0398d34ad0
1 changed files with 3 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
src/arch/arm/64/kernel/vspace.c
View File

@@ -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:
@@ -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)
{
@@ -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)) {