From ed87ba03a97f97d8bba2c4f89979e390f0dd210a Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@data61.csiro.au>
Date: Sat, 13 Apr 2019 18:34:01 +1000
Subject: [PATCH] riscv aspec: vtable roots must be page table caps

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

diff --git a/spec/abstract/RISCV64/ArchVSpace_A.thy b/spec/abstract/RISCV64/ArchVSpace_A.thy
index 08cbc11fb..3be3adee1 100644
--- a/spec/abstract/RISCV64/ArchVSpace_A.thy
+++ b/spec/abstract/RISCV64/ArchVSpace_A.thy
@@ -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]