RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

mcs: refactor validFaultHandler

Browse Source 
This changes it to be a pure function, which eases verification

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This commit is contained in:
Corey Lewis
2023-05-22 12:13:44 +10:00
committed by Gerwin Klein
parent d7f2ba4aec
commit 172d4c0f49
1 changed files with 2 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
src/object/tcb.c
View File

@@ -1030,7 +1030,6 @@ static bool_t validFaultHandler(cap_t cap)
if (!cap_endpoint_cap_get_capCanSend(cap) ||
(!cap_endpoint_cap_get_capCanGrant(cap) &&
!cap_endpoint_cap_get_capCanGrantReply(cap))) {
current_syscall_error.type = seL4_InvalidCapability;
return false;
}
break;
@@ -1038,7 +1037,6 @@ static bool_t validFaultHandler(cap_t cap)
/* just has no fault endpoint */
break;
default:
current_syscall_error.type = seL4_InvalidCapability;
return false;
}
return true;
@@ -1264,6 +1262,7 @@ exception_t decodeSetTimeoutEndpoint(cap_t cap, cte_t *slot)
/* timeout handler */
if (!validFaultHandler(thCap)) {
userError("TCB SetTimeoutEndpoint: timeout endpoint cap invalid.");
current_syscall_error.type = seL4_InvalidCapability;
current_syscall_error.invalidCapNumber = 1;
return EXCEPTION_SYSCALL_ERROR;
}
@@ -1538,6 +1537,7 @@ exception_t decodeSetSpace(cap_t cap, word_t length, cte_t *slot, word_t *buffer
/* fault handler */
if (!validFaultHandler(fhCap)) {
userError("TCB SetSpace: fault endpoint cap invalid.");
current_syscall_error.type = seL4_InvalidCapability;
current_syscall_error.invalidCapNumber = 1;
return EXCEPTION_SYSCALL_ERROR;
}