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