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