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
11(*
12    VSpace lookup code.
13*)
14
15theory VSpace_H
16imports
17  CNode_H
18  "./$L4V_ARCH/ArchVSpace_H"
19  KernelInitMonad_H
20begin
21
22context begin interpretation Arch .
23requalify_consts
24  mapKernelWindow
25  activateGlobalVSpace
26  configureTimer
27  initL2Cache
28  initIRQController
29
30  createIPCBufferFrame
31  createBIFrame
32  createFramesOfRegion
33  createITPDPTs
34  writeITPDPTs
35  createITASIDPool
36  writeITASIDPool
37  createDeviceFrames
38  handleVMFault
39  isValidVTableRoot
40  checkValidIPCBuffer
41  lookupIPCBuffer
42  vptrFromPPtr
43end
44
45#INCLUDE_HASKELL SEL4/Kernel/VSpace.lhs Arch= ONLY initKernelVM initPlatform initCPU
46
47end
48