diff --git a/include/bootinfo.h b/include/bootinfo.h index 02322e1e6d13d67be30766786efc532e4cbc4bdb..3c0f90559700541befc861a7259dbe19e38336be 100644 --- a/include/bootinfo.h +++ b/include/bootinfo.h @@ -68,7 +68,7 @@ typedef struct bi { uint8_t it_cnode_size_bits; /* initial thread's root CNode size (2^n slots) */ uint32_t num_dev_regs; /* number of device regions */ bi_dev_reg_t dev_reg_list[CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS]; /* device regions */ - uint8_t it_domain; /* initial thread's domain ID */ + dom_t it_domain; /* initial thread's domain ID */ } bi_t; /* adjust constants in config.h if this assert fails */ diff --git a/libsel4/include/sel4/bootinfo.h b/libsel4/include/sel4/bootinfo.h index 8c678a433617ba39e18b701075e2b23b3a7eb0b0..476aa41d22b066b0962a25ac430ed792d950e6a6 100644 --- a/libsel4/include/sel4/bootinfo.h +++ b/libsel4/include/sel4/bootinfo.h @@ -60,7 +60,7 @@ typedef struct { uint8_t initThreadCNodeSizeBits; /* initial thread's root CNode size (2^n slots) */ seL4_Word numDeviceRegions; /* number of device regions */ seL4_DeviceRegion deviceRegions[CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS]; /* device regions */ - uint8_t initThreadDomain; /* Initial thread's domain ID */ + uint32_t initThreadDomain; /* Initial thread's domain ID */ } seL4_BootInfo; /* function declarations */ diff --git a/src/kernel/boot.c b/src/kernel/boot.c index a7700c8f56f353f8cb4be84bf9a4ec2dc7b25a8c..1d00419d0b32e4c46dffdab37ba9e62349033edf 100644 --- a/src/kernel/boot.c +++ b/src/kernel/boot.c @@ -265,7 +265,7 @@ allocate_bi_frame( BI_PTR(pptr)->num_iopt_levels = 0; BI_PTR(pptr)->ipcbuf_vptr = ipcbuf_vptr; BI_PTR(pptr)->it_cnode_size_bits = CONFIG_ROOT_CNODE_SIZE_BITS; - BI_PTR(pptr)->it_domain = (uint8_t)ksDomSchedule[ksDomScheduleIdx].domain; + BI_PTR(pptr)->it_domain = ksDomSchedule[ksDomScheduleIdx].domain; return pptr; }