/seL4-l4v-10.1.1/HOL4/help/src-sml/ |
H A D | Lexer.lex | 9 (f text, (pos - String.size text, line), (pos, line)); 12 ((pos - String.size text, line), (pos, line)); 108 val len' = size s - 1 144 case String.fromString (String.substring (s, 1, String.size s - 2)) of 149 case Char.fromString (String.substring (s, 2, String.size s - 3)) of
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/aarch64/ |
H A D | ffi.c | 185 /* Return the size in bytes for each of the basic types. */ 369 else if (ty->size > 16) 381 return (ty->size + 7) / 8 < N_X_ARG_REG; 482 size_t size) 499 state->nsaa += size; 569 memcpy (allocate_to_stack (state, stack, ty->alignment, ty->size), 571 ty->size); 597 size_t size = alignment; local 601 /* This is the only case for which the allocated stack size 603 size 481 allocate_to_stack(struct arg_state *state, void *stack, size_t alignment, size_t size) argument 878 size_t size = ALIGN (cif->rtype->size, sizeof (UINT64)); local 1160 size_t size = ALIGN (cif->rtype->size, sizeof (UINT64)) ; local [all...] |
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Print.sml | 108 (* Words are unbreakable strings annotated with their effective size. *) 111 datatype word = Word of {word : string, size : int}; 113 fun mkWord s = Word {word = s, size = String.size s}; 119 fun spacesWord i = Word {word = nSpaces i, size = i}; 121 fun sizeWord (Word {size = x, ...}) = x; 129 datatype break = Break of {size : int, extraIndent : int}; 131 fun mkBreak n = Break {size = n, extraIndent = 0}; 133 fun sizeBreak (Break {size = x, ...}) = x; 139 fun updateSizeBreak size brea 156 val size = size1 + size2 value 781 and size = sizeChunks post value 961 and size = sizeChunks chunks value 1134 and size = 0 value 1196 and size = 0 value 1279 val size = size + topSize value 1328 val size = size + n value [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Print.sml | 108 (* Words are unbreakable strings annotated with their effective size. *) 111 datatype word = Word of {word : string, size : int}; 113 fun mkWord s = Word {word = s, size = String.size s}; 119 fun spacesWord i = Word {word = nSpaces i, size = i}; 121 fun sizeWord (Word {size = x, ...}) = x; 129 datatype break = Break of {size : int, extraIndent : int}; 131 fun mkBreak n = Break {size = n, extraIndent = 0}; 133 fun sizeBreak (Break {size = x, ...}) = x; 139 fun updateSizeBreak size brea 156 val size = size1 + size2 value 781 and size = sizeChunks post value 961 and size = sizeChunks chunks value 1134 and size = 0 value 1196 and size = 0 value 1279 val size = size + topSize value 1328 val size = size + n value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/model/ |
H A D | arm8AssemblerLib.sml | 219 mm := Int.max (!mm, String.size m) 220 ; ma := Int.max (!ma, String.size a) 249 (size, (memop, (acctype, (excl, (_, (_, (_, r)))))))), 252 size = size2 andalso memop = memop2 andalso 255 (size, (memop, (acctype, (excl, (_, (_, (_, r)))))))), 258 size = size2 andalso memop = memop2 andalso 261 (size, (memop, (acctype, (excl, (_, (_, (_, r)))))))), 264 size = size2 andalso memop = memop2 andalso 267 (size, (memop, (acctype, (excl, (_, (_, (_, r)))))))), 270 size [all...] |
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | File.C | 12 if (mode == READ) size = read(fd, buf, File_BufSize); 13 else size = -1; 44 if (mode == READ) size = read(fd, buf, File_BufSize); 45 else size = -1; 68 if (whence == SEEK_CUR) lseek64(fd, file_pos - (size - pos), SEEK_CUR); 70 size = read(fd, buf, File_BufSize); 80 return lseek64(fd, 0, SEEK_CUR) - (size - pos);
|
H A D | Solver.h | 124 int decisionLevel() const { return trail_lim.size(); } 152 for (int i = 0; i < learnts.size(); i++) remove(learnts[i], true); 153 for (int i = 0; i < clauses.size(); i++) if (clauses[i] != NULL) remove(clauses[i], true); 163 int nAssigns() { return trail.size(); } 164 int nClauses() { return clauses.size(); } 165 int nLearnts() { return learnts.size(); } 181 int nVars () { return assigns.size(); }
|
H A D | Proof.C | 34 for (int i = 0; i < files.size(); i++) 101 for (int i = 1; i < clause.size(); i++) 136 assert(chain_id.size() == chain_var.size() + 1); 138 if (chain_id.size() == 1) 152 for (int i = 0; i < chain_var.size(); i++) 270 while (dfs_stack.size()>0) { 281 int sz = chain_id.size(); 292 for (int i=0;i<chain_var.size();i++) 321 int sz = chain_id.size(); [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/tile/ |
H A D | ffi.c | 62 if (cif->rtype->size > NUM_ARG_REGS * FFI_SIZEOF_ARG) 130 memcpy(out, in, type->size); 131 return (type->size + FFI_SIZEOF_ARG - 1) / FFI_SIZEOF_ARG; 160 *argp++ = (intptr_t)(rvalue ? rvalue : alloca(cif->rtype->size)); 183 (type->size + FFI_SIZEOF_ARG - 1) / FFI_SIZEOF_ARG; 192 memcpy(argp, arg_in, type->size); 323 (type->size + FFI_SIZEOF_ARG - 1) / FFI_SIZEOF_ARG;
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | ForeignMemory.sml | 150 val freeList: {address: SysWord.word, size: word} list ref = LibrarySupport.noOverwriteRef nil 166 if #address entry ++ #size entry = #address this 168 {address= #address entry, size = #size entry + #size this } :: rest 171 else if #address this ++ #size this = #address entry 174 addFree({address= #address this, size= #size entry + #size this}, rest) 179 | findFree (space, (this as {size, addres 194 val size = Word.fromLarge(SysWord.toLarge(getAddress(addr, 0w0))) value [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/m88k/ |
H A D | obsd.S | 36 * unsigned int size); %r3 45 .size ffi_cacheflush_OBSD, . - ffi_cacheflush_OBSD 122 .size ffi_call_OBSD, . - ffi_call_OBSD 172 .size ffi_closure_OBSD,.-ffi_closure_OBSD 209 .size ffi_closure_struct_OBSD,.-ffi_closure_struct_OBSD
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/ |
H A D | pyobjc-tc.c | 47 point_type.size = 0; /*sizeof(Point);*/ 55 size_type.size = 0;/* sizeof(Size);*/ 63 rect_type.size = 0;/*sizeof(Rect);*/
|
H A D | struct3.c | 35 ts3_type.size = 0;
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
H A D | theories_dockable.scala | 117 case Some((loc, size)) => 118 loc0.x + loc.x <= p.x && p.x < loc0.x + size.width && 119 loc0.y + loc.y <= p.y && p.y < loc0.y + size.height 143 if (location != null && size != null) 144 checkbox_geometry = Some((location, size)) 160 gfx.fillRect(x, 0, w, size.height) 163 paint_segment(0, size.width, background) 174 ((size.width - 2) /: segments)({ case (last, (n, color)) => 175 val w = (n * ((size.width - 4) - segments.length) / st.total) max 4 181 paint_segment(0, size [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | theories_dockable.scala | 117 case Some((loc, size)) => 118 loc0.x + loc.x <= p.x && p.x < loc0.x + size.width && 119 loc0.y + loc.y <= p.y && p.y < loc0.y + size.height 143 if (location != null && size != null) 144 checkbox_geometry = Some((location, size)) 160 gfx.fillRect(x, 0, w, size.height) 163 paint_segment(0, size.width, background) 174 ((size.width - 2) /: segments)({ case (last, (n, color)) => 175 val w = (n * ((size.width - 4) - segments.length) / st.total) max 4 181 paint_segment(0, size [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/HOL4/polyml/libpolyml/libffi/src/powerpc/ |
H A D | ffi_linux64.c | 47 /* Adjust size of ffi_type_longdouble. */ 53 ffi_type_longdouble.size = 8; 58 ffi_type_longdouble.size = 16; 173 if (cif->rtype->size <= 16) 224 intarg_count += ((*ptr)->size + 7) / 8; 590 words = ((*ptr)->size + 7) / 8; 595 memcpy (rest.c, *p_argv.c + first, (*ptr)->size - first); 603 /* Structures with size less than eight bytes are passed 605 if ((*ptr)->size < 8) 606 where += 8 - (*ptr)->size; 658 flush_icache(char *wraddr, char *xaddr, int size) argument [all...] |
H A D | ffi_sysv.c | 45 /* Adjust size of ffi_type_longdouble. */ 51 ffi_type_longdouble.size = 8; 56 ffi_type_longdouble.size = 16; 100 unsigned size = cif->rtype->size; local 113 - Structures of size <= 4 bytes also returned in gpr3; 153 if ((cif->abi & FFI_SYSV_STRUCT_RET) != 0 && size <= 8) 239 struct_copy_size += ((*ptr)->size + 15) & ~0xF; 573 struct_copy_size = ((*ptr)->size + 15) & ~0xF; 575 memcpy (copy_space.c, *p_argv.c, (*ptr)->size); 632 flush_icache(char *wraddr, char *xaddr, int size) argument 703 unsigned size = cif->rtype->size; local [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | memmgr.cpp | 81 bool LocalMemSpace::InitSpace(POLYUNSIGNED size, bool mut) argument 86 size_t iSpace = size*sizeof(PolyWord); 94 // The size may have been rounded up to a block boundary. 95 size = iSpace/sizeof(PolyWord); 97 top = bottom + size; 107 return bitmap.Create(size); 139 LocalMemSpace* MemMgr::NewLocalSpace(POLYUNSIGNED size, bool mut) argument 160 bool success = space->InitSpace(size, mut) && AddLocalSpace(space); 165 Log("MMGR: New local %smutable space %p, size=%luk words, bottom=%p, top=%p\n", mut ? "": "im", 186 LocalMemSpace *MemMgr::CreateAllocationSpace(POLYUNSIGNED size) argument 308 NewExportSpace(POLYUNSIGNED size, bool mut, bool noOv, bool code) argument 590 NewCodeSpace(POLYUNSIGNED size) argument 781 NewStackSpace(POLYUNSIGNED size) argument [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/arc/ |
H A D | ffi.c | 78 z = (*p_arg)->size; 102 memcpy (argp, *p_argv, (*p_arg)->size); 178 ecif.rvalue = alloca (cif->rtype->size); 230 z = (*p_argt)->size;
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/ |
H A D | debug.c | 55 FFI_ASSERT_AT(a->type == FFI_TYPE_VOID || a->size > 0, file, line);
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/x86/ |
H A D | ffi.c | 68 && ((ecif->cif->rtype->size & (1 | 2 | 4 | 8)) == 0) 106 size_t z = (*p_arg)->size; 170 are the first two none-floating-point arguments with a size 270 if (cif->rtype->size == 1) 272 cif->flags = FFI_TYPE_SMALL_STRUCT_1B; /* same as char size */ 274 else if (cif->rtype->size == 2) 276 cif->flags = FFI_TYPE_SMALL_STRUCT_2B; /* same as short size */ 278 else if (cif->rtype->size == 4) 286 else if (cif->rtype->size == 8) 320 cif->bytes += (unsigned)ALIGN((*ptr)->size, FFI_SIZEOF_AR [all...] |
/seL4-l4v-10.1.1/seL4/include/arch/arm/arch/64/mode/machine/ |
H A D | hardware.h | 30 #error Unable to determine L1 cache line size 76 fail("Invalid page size");
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/test/ |
H A D | regexTest.sml | 84 fun getPerformanceTests file size = 86 val longString = readFile file size; 102 fun getPerformanceTestsRegexSize file size regexLength = 104 val longString = readFile file size;
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | base_tokens.sml | 48 val c = String.sub (s, size s - 1) 53 then (String.substring(s,0,size s - 1), SOME c) 56 if String.sub(s, 0) <> #"0" orelse size s = 1 then 89 places = String.size fpart}
|