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 "Retyping Objects" 12 13theory Retype_H 14imports 15 RetypeDecls_H 16 Endpoint_H 17 Untyped_H 18 Interrupt_H 19begin 20 21context Arch begin 22requalify_consts 23 deriveCap finaliseCap postCapDeletion isCapRevocable 24 hasCancelSendRights sameRegionAs isPhysicalCap 25 sameObjectAs updateCapData maskCapRights 26 createObject capUntypedPtr capUntypedSize 27 performInvocation decodeInvocation prepareThreadDelete 28 cteRightsBits cteGuardBits 29 30context begin global_naming global 31 32requalify_consts 33 RetypeDecls_H.deriveCap RetypeDecls_H.finaliseCap RetypeDecls_H.postCapDeletion 34 RetypeDecls_H.hasCancelSendRights RetypeDecls_H.sameRegionAs RetypeDecls_H.isPhysicalCap 35 RetypeDecls_H.sameObjectAs RetypeDecls_H.updateCapData RetypeDecls_H.maskCapRights 36 RetypeDecls_H.createObject RetypeDecls_H.capUntypedPtr RetypeDecls_H.capUntypedSize 37 RetypeDecls_H.performInvocation RetypeDecls_H.decodeInvocation RetypeDecls_H.isCapRevocable 38end 39 40end 41 42#INCLUDE_HASKELL SEL4/Object/ObjectType.lhs Arch=Arch bodies_only 43 44end 45