From 8ab955984f2d1ebe66add9f9d226a52cd6bcf6ac Mon Sep 17 00:00:00 2001
From: Matthew Brecknell <Matthew.Brecknell@nicta.com.au>
Date: Tue, 26 Apr 2016 13:45:59 +1000
Subject: [PATCH] arch_split: CSpec checking

---
 spec/cspec/Kernel_C.thy | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/spec/cspec/Kernel_C.thy b/spec/cspec/Kernel_C.thy
index df392cf93..4424030bb 100644
--- a/spec/cspec/Kernel_C.thy
+++ b/spec/cspec/Kernel_C.thy
@@ -15,8 +15,13 @@ imports
   "../../tools/asmrefine/CommonOps"
 begin
 
+unqualify_types (in Arch)
+  machine_state
+
 declare [[populate_globals=true]]
 
+context begin interpretation ARM . (*FIXME: arch_split*)
+
 type_synonym cghost_state = "(machine_word \<rightharpoonup> vmpage_size) * (machine_word \<rightharpoonup> nat)
     * ghost_assertions"
 
@@ -57,6 +62,8 @@ abbreviation
 declare [[record_codegen = false]]
 declare [[allow_underscore_idents = true]]
 
+end
+
 install_C_file "c/kernel_all.c_pp"
   [machinety=machine_state, ghostty=cghost_state]