From d82b9f0434e5ef581e029756af918d41ecb93289 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Tue, 24 Nov 2020 00:36:04 +1100 Subject: [PATCH] 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 --- include/arch/arm/arch/machine/gic_v3.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/include/arch/arm/arch/machine/gic_v3.h b/include/arch/arm/arch/machine/gic_v3.h index 2310ef759..7d1a1c01d 100644 --- a/include/arch/arm/arch/machine/gic_v3.h +++ b/include/arch/arm/arch/machine/gic_v3.h @@ -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;