arm: DONT_TRANSLATE isIRQPending for GIC v3

This is a shortcut for dealing with the inline assembly inside to
prevent the modifies analysis from picking up every part of the state.

For any future binary correctness analysis, this will need to be
removed, and instead an appeal made to inline assembly being unable to
modify the heap.

Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
This commit is contained in:
Rafal Kolanski
2020-11-24 00:36:04 +11:00
parent 39a4d68d84
commit d82b9f0434

View File

@@ -257,6 +257,8 @@ static inline interrupt_t getActiveIRQ(void)
* seL4 expects two states: active->inactive.
* We ignore the active state in GIC to conform
*/
/** MODIFIES: phantom_machine_state */
/** DONT_TRANSLATE */
static inline bool_t isIRQPending(void)
{
uint32_t val = 0;