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

x64: abstract: fixup arch_same_region_as for IOPorts

This commit is contained in:
Joel Beeren 2017-03-30 13:09:40 +11:00
parent 659088cc13
commit 1e8228700b
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/ArchCSpace_A.thy
View File

@ -72,7 +72,7 @@ where
--"FIXME: should this also check domain id equality? C kernel does not"
*)
| "arch_same_region_as (IOPortCap frst lst) c' =
(\<exists>frst' lst'. c' = IOPortCap frst' lst' \<and> frst \<le> frst' \<and> lst' \<le> lst)"
(\<exists>frst' lst'. c' = IOPortCap frst' lst' \<and> frst \<le> frst' \<and> lst' \<le> lst \<and> frst' \<le> lst')"
text {* Check whether two arch capabilities are to the same object. *}
definition