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

riscv aspec: vtable roots must be page table caps

This commit is contained in:
Gerwin Klein 2019-04-13 18:34:01 +10:00 committed by Rafal Kolanski
parent c386d2a85e
commit ed87ba03a9
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
spec/abstract/RISCV64/ArchVSpace_A.thy
View File

@ -243,7 +243,7 @@ text \<open>
definition is_valid_vtable_root :: "cap \<Rightarrow> bool"
where
"is_valid_vtable_root c \<equiv>
case c of ArchObjectCap (FrameCap _ _ _ _ (Some _)) \<Rightarrow> True | _ \<Rightarrow> False"
case c of ArchObjectCap (PageTableCap _ (Some _)) \<Rightarrow> True | _ \<Rightarrow> False"
text \<open>Make numeric value of @{const msg_align_bits} visible.\<close>
lemmas msg_align_bits = msg_align_bits'[unfolded word_size_bits_def, simplified]