secc
/
seL4-L4.verified
mirror of https://github.com/seL4/l4v.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

arm+arm-hyp+aarch64 machine: fix GICv3 gicNumTargets_bits 

The value of gicNumTargets_bits was wrong for GICv3 platforms, breaking
CRefine for those platforms.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2025-07-07 15:10:49 +10:00
parent b35045a477
commit be238597cc
3 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
spec/machine/AARCH64/Platform.thy
View File

@ -37,7 +37,7 @@ definition numSGIs :: nat where
"numSGIs = 2^numSGIs_bits"
definition gicNumTargets_bits :: nat where
"gicNumTargets_bits \<equiv> if Kernel_Config.config_ARM_GIC_V3 then 5 else 3"
"gicNumTargets_bits \<equiv> if Kernel_Config.config_ARM_GIC_V3 then 4 else 3"
definition gicNumTargets :: nat where
"gicNumTargets \<equiv> 2^gicNumTargets_bits"

2
spec/machine/ARM/Platform.thy
View File

@ -44,7 +44,7 @@ definition numSGIs :: nat where
"numSGIs = 2^numSGIs_bits"
definition gicNumTargets_bits :: nat where
"gicNumTargets_bits \<equiv> if Kernel_Config.config_ARM_GIC_V3 then 5 else 3"
"gicNumTargets_bits \<equiv> if Kernel_Config.config_ARM_GIC_V3 then 4 else 3"
definition gicNumTargets :: nat where
"gicNumTargets \<equiv> 2^gicNumTargets_bits"

2
spec/machine/ARM_HYP/Platform.thy
View File

@ -44,7 +44,7 @@ definition numSGIs :: nat where
"numSGIs = 2^numSGIs_bits"
definition gicNumTargets_bits :: nat where
"gicNumTargets_bits \<equiv> if Kernel_Config.config_ARM_GIC_V3 then 5 else 3"
"gicNumTargets_bits \<equiv> if Kernel_Config.config_ARM_GIC_V3 then 4 else 3"
definition gicNumTargets :: nat where
"gicNumTargets \<equiv> 2^gicNumTargets_bits"