| /* |
| * 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) |
| } |
| } |
