arm,gic_v2: minor rephrasing for verification

The proofs are shared between GICv2 and GICv3, which means we want the
term structure to be the same for key functions that are visible to the
proofs (but constants are Ok to change).

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2025-11-19 14:39:44 +11:00
parent e0abb976b5
commit 5f62269d84

View file

@ -177,7 +177,8 @@ BOOT_CODE void cpu_initLocalIRQController(void)
bool_t plat_SGITargetValid(word_t target)
{
return target < GIC_SGI_NUM_TARGETS;
/* written as <= so that the term is the same as in gic_v3 for the proofs */
return target <= GIC_SGI_NUM_TARGETS - 1;
}
void plat_sendSGI(word_t irq, word_t target)