adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

aarch64 machine: introduce irq_len 

Make it possible to refer to the size of the irq type symbolically.
So far, this is only necessary in an example state for kernel init,
but it's still nicer to avoid magic numbers.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-02-06 09:13:25 +11:00
parent d43aa2e296
commit 1e4b3d7573
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -17,7 +17,8 @@ begin
context Arch begin global_naming AARCH64
type_synonym irq = "9 word" (* match IRQ_CNODE_SLOT_BITS in seL4 config *)
type_synonym irq_len = 9 (* match IRQ_CNODE_SLOT_BITS in seL4 config *)
type_synonym irq = "irq_len word"
type_synonym paddr = machine_word
abbreviation (input) "toPAddr \<equiv> id"