The computation in mcsPreemptionPoint no longer depends on the irq, so getActiveIRQ() can be called closer to the actual use site of the irq. This makes things slightly easier for verification because we don't need to reason about potential side effects of mcsPreemptionPoint before the irq value is used. Closes #472 Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems> |
||
|---|---|---|
| .. | ||
| faults.c | ||
| syscall.c | ||