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

arch_split: CSpec checking

This commit is contained in:
Matthew Brecknell 2016-04-26 13:45:59 +10:00
parent 03b7ec7db0
commit 8ab955984f
1 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
spec/cspec/Kernel_C.thy
View File

@ -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]