/seL4-l4v-10.1.1/seL4/libsel4/tools/ |
H A D | bitfield_gen.py | 42 # Isabelle word size suffixes for return value names 1184 def field_mask_proof(base, base_bits, sign_extend, high, size): 1188 return "NOT (mask %d)" % (base_bits - size) 1190 return "(mask %d << %d)" % (size, base_bits - size) 1192 return "mask %d" % size 1225 # Ensure that block sizes and tag size & position match for 1239 union_size = ref.size 1240 elif union_size != ref.size: 1383 offset, size, hig [all...] |
/seL4-l4v-10.1.1/seL4/manual/tools/libsel4_tools/ |
H A D | bitfield_gen.py | 42 # Isabelle word size suffixes for return value names 1184 def field_mask_proof(base, base_bits, sign_extend, high, size): 1188 return "NOT (mask %d)" % (base_bits - size) 1190 return "(mask %d << %d)" % (size, base_bits - size) 1192 return "mask %d" % size 1225 # Ensure that block sizes and tag size & position match for 1239 union_size = ref.size 1240 elif union_size != ref.size: 1383 offset, size, hig [all...] |
/seL4-l4v-10.1.1/seL4/tools/ |
H A D | bitfield_gen.py | 42 # Isabelle word size suffixes for return value names 1184 def field_mask_proof(base, base_bits, sign_extend, high, size): 1188 return "NOT (mask %d)" % (base_bits - size) 1190 return "(mask %d << %d)" % (size, base_bits - size) 1192 return "mask %d" % size 1225 # Ensure that block sizes and tag size & position match for 1239 union_size = ref.size 1240 elif union_size != ref.size: 1383 offset, size, hig [all...] |
/seL4-l4v-10.1.1/seL4/src/ |
H A D | string.c | 22 word_t strlcpy(char *dest, const char *src, word_t size) argument 25 for (len = 0; len + 1 < size && src[len]; len++) { 32 word_t strlcat(char *dest, const char *src, word_t size) argument 36 for (len = 0; len < size && dest[len]; len++); 37 /* check that dest was at least 'size' length to prevent inserting 39 if (len < size) { 40 for (; len + 1 < size && *src; len++, src++) {
|
/seL4-l4v-10.1.1/seL4/src/plat/spike/machine/ |
H A D | fdt.c | 172 uint64_t base, size; local 174 value = fdt_get_size (node->parent, value, &size); 176 base, base + size 178 printf("Failed to add physical memory region %llu-%llu\n", (unsigned long long)base, (unsigned long long)(base + size));
|
/seL4-l4v-10.1.1/seL4/src/object/ |
H A D | tcb.c | 473 word_t vaddr, word_t type, word_t size, word_t rw) 475 setBreakpoint(tcb, bp_num, vaddr, type, size, rw); 485 word_t vaddr, type, size, rw; local 493 size = getSyscallArg(3, buffer); 514 if (size != 0) { 515 userError("Debug: Instruction bps must have size of 0."); 534 if (size == 0) { 535 userError("Debug: Data bps cannot have size of 0."); 561 if (size != 0 && size ! 472 invokeSetBreakpoint(tcb_t *tcb, uint16_t bp_num, word_t vaddr, word_t type, word_t size, word_t rw) argument [all...] |
/seL4-l4v-10.1.1/seL4/src/arch/x86/object/ |
H A D | ioport.c | 40 ensurePortOperationAllowed(cap_t cap, uint32_t start_port, uint32_t size) argument 44 uint32_t end_port = start_port + size - 1; 294 /* We construct the value for data from raw_data based on the actual size of the port 297 cast down to the correct word size removing the extra here is currently relied upon
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/machine/ |
H A D | breakpoint.c | 204 /** Converts an integer size number into an equivalent hardware register value. 207 * @param size An integer for the operand size of the breakpoint. 211 convertSizeToArch(uint16_t bp_num, word_t type, word_t size) argument 218 size = 0; 220 switch (size) { 222 size = X86_DEBUG_BP_SIZE_1B; 225 size = X86_DEBUG_BP_SIZE_2B; 228 size = X86_DEBUG_BP_SIZE_8B; 231 assert(size 423 setBreakpoint(tcb_t *t, uint16_t bp_num, word_t vaddr, word_t types, word_t size, word_t rw) argument [all...] |
/seL4-l4v-10.1.1/seL4/src/arch/x86/kernel/ |
H A D | boot_sys.c | 71 uint32_t mem_lower; /* lower memory size for boot code of APs to run in real mode */ 143 printf("size=0x%lx v_entry=%p v_start=%p v_end=%p ", 291 printf("\tPhysical Memory Region from %lx size %lx type %d\n", (long)mem_start, (long)mem_length, type); 453 printf("Kernel loaded to: start=0x%lx end=0x%lx size=0x%lx entry=0x%lx\n", 525 "Moving loaded userland images to final location: from=0x%lx to=0x%lx size=0x%lx\n", 578 printf("Boot loader did not provide information about physical memory size\n"); 596 " module #%ld: start=0x%x end=0x%x size=0x%x name='%s'\n", 604 printf("Invalid boot module size! Possible cause: boot module file not found by QEMU\n"); 694 if (ACPI_V1_SIZE == tag->size - sizeof(*tag)) { 695 memcpy(&boot_state.acpi_rsdp, (void *)behind_tag, tag->size [all...] |
/seL4-l4v-10.1.1/seL4/src/arch/x86/64/ |
H A D | traps.S | 20 * The size of interrupt-stack pushes is fixed at 64 bits; and the processor uses 8-byte, zero extended 172 .size int_##number, . - int_##number;
|
/seL4-l4v-10.1.1/seL4/src/arch/arm/object/ |
H A D | iospace.c | 461 word_t size = BIT((SMMU_PD_INDEX_BITS)); local 465 memset((void *)pd, 0, size); 466 cleanCacheRange_RAM((word_t)pd, (word_t)pd + size, addrFromPPtr(pd));
|
/seL4-l4v-10.1.1/seL4/src/arch/arm/machine/ |
H A D | debug.c | 434 /** Convert a watchpoint size (0, 1, 2, 4 or 8 bytes) into the arch specific 438 convertSizeToArch(word_t size) argument 440 switch (size) { 448 assert(size == 4); 453 /** Convert an arch specific encoded watchpoint size back into a simple integer 549 * @params vaddr, type, size, rw: seL4 API values for seL4_TCB_SetBreakpoint. 555 word_t vaddr, word_t type, word_t size, word_t rw) 601 wcr = dbg_wcr_set_byteAddressSelect(wcr, convertSizeToArch(size)); 636 ret.size = 0; 644 ret.size 553 setBreakpoint(tcb_t *t, uint16_t bp_num, word_t vaddr, word_t type, word_t size, word_t rw) argument [all...] |
/seL4-l4v-10.1.1/seL4/src/arch/arm/armv/armv8-a/64/ |
H A D | cache.c | 50 word_t size, csselr_old; local 55 /* Read 'size' */ 56 MRS("ccsidr_el1", size); 59 return size;
|
/seL4-l4v-10.1.1/seL4/src/arch/arm/64/kernel/ |
H A D | vspace.c | 39 * 8-bit VMID. Note that this assumes that the IPA size for S2 276 /* verify that the kernel device window is 1gb aligned and 1gb in size */ 1492 word_t size = end - start; local 1494 end = start + size; 1663 word_t size = end - start; local 1665 end = start + size;
|
/seL4-l4v-10.1.1/seL4/src/arch/arm/32/kernel/ |
H A D | vspace.c | 41 * looking at the size difference of the mappings, and is done this way to remove magic 1864 pageBase(vptr_t vaddr, vm_page_size_t size) argument 1866 return vaddr & ~MASK(pageBitsForSize(size)); 3018 userError("Invalid frame size. The kernel expects 1M log buffer");
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | vspace.tex | 40 The size and type of structure at each level, and the number of bits in the virtual address resolved 157 the size of the \obj{Page} and must be mapped to a suitable VSpace, and every intermediate paging
|
H A D | objects.tex | 252 is a word-size array of flags, each of which behaves like a binary semaphore. Operations 400 \texttt{size\_bits} argument to 402 the size of the resulting objects. 403 For all other object types, the size is fixed, and the \texttt{size\_bits} 410 the case of variable-sized objects, each object must also be of the same size. 411 If the size of the memory area needed (calculated by the object size multiplied
|
H A D | cspace.tex | 319 the power to which two is raised in its size. That is, if a \obj{CNode} has 403 together with a window size parameter, specifying the number of slots 442 of 0x00F00060 and a window size of 5. 462 slots, the user supplies a starting address and a window size. 520 When resolving a capability, a CNode was traversed with a guard size 531 \ipcbloc{Offset + seL4\_CapFault\_GuardMismatch\_BitsFound} & The CNode's guard size \\
|
H A D | intro.tex | 27 confidentiality~\cite{Murray_MBGBSLGK_13}. The kernel's small size was
|
H A D | bootup.tex | 22 The CNode size can be configured at compile time (default is $2^{12}$ 67 bootstrapping. Their exact contents depend on the userland image size, 106 \texttt{seL4\_Uint8} & \texttt{initThreadCNodeSizeBits} & CNode size ($2^n$ slots) \\ 144 of paging structure size. Within a given paging structure size, capabilities are 170 in \autoref{tab:untyped_desc_struct}, and details the address, size and kind of 185 \texttt{seL4\_Uint8} & \texttt{padding1} & manual padding so final struct is a multiple of the word size \\ 186 \texttt{seL4\_Uint8} & \texttt{padding2} & manual padding so final struct is a multiple of the word size \\ 187 \texttt{seL4\_Uint8} & \texttt{sizeBits} & size ($2^n$ bytes) of the untyped object \\
|
H A D | api.tex | 91 '\texttt{seL4\_Word size}', integer value for the span-size of the breakpoint.
|
/seL4-l4v-10.1.1/seL4/include/api/ |
H A D | macros.h | 21 * the same size as a 'long'. 55 #define SEL4_SIZE_SANITY(index, entry, size) SEL4_COMPILE_ASSERT(index##entry##size, index + entry == size)
|
/seL4-l4v-10.1.1/seL4/libsel4/include/sel4/ |
H A D | macros.h | 21 * the same size as a 'long'. 55 #define SEL4_SIZE_SANITY(index, entry, size) SEL4_COMPILE_ASSERT(index##entry##size, index + entry == size)
|
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/api/ |
H A D | bootinfo_types.h | 126 uint32_t size; // size of this struct in bytes member in struct:seL4_X86_mb_mmap
|
/seL4-l4v-10.1.1/seL4/libsel4/arch_include/x86/sel4/arch/ |
H A D | bootinfo_types.h | 126 uint32_t size; // size of this struct in bytes member in struct:seL4_X86_mb_mmap
|