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

Isabelle2018 arm: ExecSpec

This commit is contained in:
Gerwin Klein 2018-06-22 14:16:59 +02:00
parent 75b38be012
commit 3525eb6d15
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/design/m-skel/ARM/MachineTypes.thy
View File

@ -129,7 +129,7 @@ definition
"init_machine_state \<equiv> \<lparr> irq_masks = init_irq_masks,
irq_state = 0,
underlying_memory = init_underlying_memory,
device_state = empty,
device_state = Map.empty,
exclusive_state = default_exclusive_state,
machine_state_rest = undefined \<rparr>"

2
spec/design/m-skel/ARM_HYP/MachineTypes.thy
View File

@ -131,7 +131,7 @@ definition
"init_machine_state \<equiv> \<lparr> irq_masks = init_irq_masks,
irq_state = 0,
underlying_memory = init_underlying_memory,
device_state = empty,
device_state = Map.empty,
exclusive_state = default_exclusive_state,
machine_state_rest = undefined \<rparr>"

2
spec/design/m-skel/X64/MachineTypes.thy
View File

@ -105,7 +105,7 @@ definition
"init_machine_state \<equiv> \<lparr> irq_masks = init_irq_masks,
irq_state = 0,
underlying_memory = init_underlying_memory,
device_state = empty,
device_state = Map.empty,
machine_state_rest = undefined \<rparr>"
#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs CONTEXT X64 ONLY VMFaultType HypFaultType VMPageSize VMMapType pageBits ptTranslationBits pageBitsForSize