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 "Physical Memory Functions"
12
13theory PSpaceFuns_H
14imports
15  ObjectInstances_H
16  FaultMonad_H
17  "Lib.DataMap"
18begin
19
20context begin interpretation Arch .
21requalify_consts
22  fromPPtr
23  PPtr
24  freeMemory
25  storeWord
26  loadWord
27end
28
29definition deleteRange :: "( machine_word , 'a ) DataMap.map \<Rightarrow> machine_word \<Rightarrow> nat \<Rightarrow> ( machine_word , 'a ) DataMap.map"
30where "deleteRange m ptr bits \<equiv>
31        let inRange = (\<lambda> x. x && ((- mask bits) - 1) = fromPPtr ptr) in
32        data_map_filterWithKey (\<lambda> x _. Not (inRange x)) m"
33
34#INCLUDE_HASKELL SEL4/Model/PSpace.lhs decls_only Data.Map=DataMap NOT PSpace ptrBits ptrBitsForSize lookupAround maybeToMonad lookupAround2 typeError alignError alignCheck sizeCheck objBits deleteRange
35
36consts
37lookupAround2 :: "('k :: {linorder,finite}) \<Rightarrow> ( 'k , 'a ) DataMap.map \<Rightarrow> (('k * 'a) option * 'k option)"
38
39#INCLUDE_HASKELL SEL4/Model/PSpace.lhs bodies_only Data.Map=DataMap NOT PSpace ptrBits ptrBitsForSize lookupAround maybeToMonad typeError alignError alignCheck sizeCheck objBits deletionIsSafe cNodePartialOverlap pointerInUserData ksASIDMapSafe deleteRange
40
41end
42