From 1e8228700bce3b5fffac6935af0a77b8ae1dcdae Mon Sep 17 00:00:00 2001
From: Joel Beeren <joel.beeren@nicta.com.au>
Date: Thu, 30 Mar 2017 13:09:40 +1100
Subject: [PATCH] x64: abstract: fixup arch_same_region_as for IOPorts

---
 spec/abstract/X64/ArchCSpace_A.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/spec/abstract/X64/ArchCSpace_A.thy b/spec/abstract/X64/ArchCSpace_A.thy
index d1df2971b..e1d440172 100644
--- a/spec/abstract/X64/ArchCSpace_A.thy
+++ b/spec/abstract/X64/ArchCSpace_A.thy
@@ -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