1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 *)
10
11chapter "CSpace"
12
13theory CSpace_H
14imports CSpaceDecls_H Object_H
15begin
16
17#INCLUDE_HASKELL SEL4/Kernel/CSpace.lhs bodies_only NOT resolveAddressBits
18
19
20function
21  resolveAddressBits ::
22  "capability \<Rightarrow> cptr \<Rightarrow> nat \<Rightarrow>
23   (lookup_failure, (machine_word * nat)) kernel_f"
24where
25 "resolveAddressBits a b c =
26#INCLUDE_HASKELL SEL4/Kernel/CSpace.lhs BODY resolveAddressBits
27a b c"
28  by auto
29
30termination
31  apply (relation "measure (snd o snd)")
32  apply (auto simp add: in_monad split: if_split_asm)
33  done
34
35defs
36  resolveAddressBits_decl_def [simp]:
37  "CSpaceDecls_H.resolveAddressBits \<equiv> resolveAddressBits"
38
39end
40