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 ArchVSpace_H 16imports 17 "../CNode_H" 18 "../Untyped_H" 19 "../KI_Decls_H" 20 ArchVSpaceDecls_H 21begin 22 23context Arch begin global_naming X64_H 24 25#INCLUDE_HASKELL SEL4/Kernel/VSpace/X64.lhs CONTEXT X64_H bodies_only ArchInv=ArchRetypeDecls_H NOT checkPML4At checkPDPTAt checkPDAt checkPTAt checkValidMappingSize 26#INCLUDE_HASKELL SEL4/Object/IOPort/X64.lhs CONTEXT X64_H bodies_only ArchInv=ArchRetypeDecls_H 27 28defs checkValidMappingSize_def: 29 "checkValidMappingSize sz \<equiv> stateAssert 30 (\<lambda>s. 2 ^ pageBitsForSize sz <= gsMaxObjectSize s) []" 31 32end 33 34end 35