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

x64 aspec: trivial - removed filename prefix in set_asid_pool definition

This commit is contained in:
Victor Phan 2019-04-12 14:22:26 +10:00
parent 1fd4c1ab0b
commit 1c35127dcc
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/X64/ArchVSpaceAcc_A.thy
View File

@ -56,7 +56,7 @@ definition
definition
set_asid_pool :: "obj_ref \<Rightarrow> (asid_low_index \<rightharpoonup> obj_ref) \<Rightarrow> (unit, 'z::state_ext) s_monad" where
"set_asid_pool ptr pool \<equiv> set_object ptr (ArchObj (arch_kernel_obj.ASIDPool pool))"
"set_asid_pool ptr pool \<equiv> set_object ptr (ArchObj (ASIDPool pool))"
definition
get_pd :: "obj_ref \<Rightarrow> (9 word \<Rightarrow> pde,'z::state_ext) s_monad" where