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

riscv aspec: make aobjs_of projection available in generic spec

This commit is contained in:
Rafal Kolanski 2019-03-08 15:29:22 +11:00
parent ab23a6bd45
commit 3e8f89f249
2 changed files with 6 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
spec/abstract/KHeap_A.thy
View File

@ -21,6 +21,12 @@ begin
text \<open>This theory gives auxiliary getter and setter methods
for kernel objects.\<close>
section "Projections of the Kernel Heap"
abbreviation aobjs_of :: "'z::state_ext state \<Rightarrow> obj_ref \<rightharpoonup> arch_kernel_obj"
where
"aobjs_of \<equiv> \<lambda>s. kheap s |> aobj_of"
section "General Object Access"
definition

4
spec/abstract/RISCV64/ArchVSpaceAcc_A.thy
View File

@ -44,10 +44,6 @@ section "Kernel Heap Accessors"
text \<open>Manipulate ASID pools, page directories and page tables in the kernel heap.\<close>
locale_abbrev aobjs_of :: "'z::state_ext state \<Rightarrow> obj_ref \<rightharpoonup> arch_kernel_obj"
where
"aobjs_of \<equiv> \<lambda>s. kheap s |> aobj_of"
locale_abbrev asid_pools_of :: "'z::state_ext state \<Rightarrow> obj_ref \<rightharpoonup> asid_pool"
where
"asid_pools_of \<equiv> \<lambda>s. aobjs_of s |> asid_pool_of"