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