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

arm,sgi: wrap NUM_SGIS for verification

Browse Source 
Wrap NUM_SGIS using wrap_config_set() so that verification automation
does not simplify it away automatically when it is 0.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein
2025-08-23 21:20:14 +01:00
parent 0f78e4e957
commit 08fb719ca2
1 changed files with 5 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
src/arch/arm/object/interrupt.c
View File

@@ -96,7 +96,8 @@ exception_t Arch_decodeIRQControlInvocation(word_t invLabel, word_t length,
return EXCEPTION_SYSCALL_ERROR;
}
// wrap_config_set to prevent verification automation from simplifying it away
/* wrap_config_set to prevent verification automation from simplifying
away the condition when NUM_SGIS = 0 */
if (wrap_config_set(NUM_SGIS) == 0) {
current_syscall_error.type = seL4_IllegalOperation;
userError("IRQControl: IssueSGISignal not available on this platform.");
@@ -110,7 +111,9 @@ exception_t Arch_decodeIRQControlInvocation(word_t invLabel, word_t length,
cap_t cnodeCap = current_extra_caps.excaprefs[0]->cap;
if (irq >= NUM_SGIS) {
/* wrap_config_set to prevent verification automation from simplifying
away the condition when NUM_SGIS = 0 */
if (irq >= wrap_config_set(NUM_SGIS)) {
current_syscall_error.type = seL4_RangeError;
current_syscall_error.rangeErrorMin = 0;
current_syscall_error.rangeErrorMax = NUM_SGIS - 1;