| /* | |
| * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) | |
| * | |
| * SPDX-License-Identifier: BSD-2-Clause | |
| */ | |
| arch ia32 | |
| objects { | |
| cnode = cnode (4 bits) | |
| tcb = tcb (addr: 0x15000, ip: 0x00010000, sp: 0x00013000, prio: 42, max_prio: 254, affinity: 0, init:[10,15], fault_ep: 1) | |
| pd1 = pd | |
| ap = asid_pool (asid_high: 0x1) | |
| pt1 = pt | |
| frame[6] = frame (4k) | |
| ep = notification | |
| cnode2 = cnode (4 bits) | |
| } | |
| caps { | |
| cnode { | |
| tcb | |
| ep (RWG) | |
| cnode (guard: 0, guard_size: 28) | |
| frame[5] (RWG) | |
| } | |
| ap { pd1 } | |
| pd1 { 0: pt1 } | |
| pt1 { | |
| 0x10: frame[] (RWG) | |
| } | |
| cnode2 { 5: cnode (guard: 1, guard_size: 28) } | |
| tcb { | |
| cspace: cnode2 (guard: 0, guard_size: 28) | |
| vspace: pd1 | |
| ipc_buffer_slot: frame[5] (RWG) | |
| } | |
| } |