michaelmcinerney
michaelmcinerney
This factors out code from cancelAllIPC and cancelBadgedSends by introducing the inline function restart_thread_if_no_fault
This refactors refill_budget_check and schedule_used to ease verification by limiting heap access via refill_head and refill_tail, and providing (inlined) named functions for both the condition and bodies of the loops.
Test with https://github.com/seL4/seL4/pull/1312
`stateAssert` is currently used within the design spec to assert properties about the state. However, given that we do not translate the string associated with the Haskell `assert` into the...