/seL4-l4v-master/isabelle/src/Pure/ |
H A D | thm_name.scala | 19 case 0 => thm_name1.index compare thm_name2.index 30 case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index) 35 sealed case class Thm_Name(name: String, index: Int) 38 if (name == "" || index == 0) name 39 else name + "(" + index + ")" 42 if (name == "" || index == 0) name 43 else name + "_" + index
|
/seL4-l4v-master/l4v/isabelle/src/Pure/ |
H A D | thm_name.scala | 19 case 0 => thm_name1.index compare thm_name2.index 30 case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index) 35 sealed case class Thm_Name(name: String, index: Int) 38 if (name == "" || index == 0) name 39 else name + "(" + index + ")" 42 if (name == "" || index == 0) name 43 else name + "_" + index
|
/seL4-l4v-master/seL4/src/arch/arm/machine/ |
H A D | cache.c | 18 word_t index; local 20 for (index = LINE_INDEX(start); index < LINE_INDEX(end) + 1; index++) { 21 line = index << L1_CACHE_LINE_SIZE_BITS; 29 word_t index; local 47 for (index = LINE_INDEX(start); index < LINE_INDEX(end) + 1; index++) { 48 line = index << L1_CACHE_LINE_SIZE_BIT 80 word_t index; local 96 word_t index; local 138 word_t index; local 149 word_t index; local [all...] |
/seL4-l4v-master/seL4/include/arch/x86/arch/64/mode/model/ |
H A D | smp.h | 27 cpu_id_t index; member in struct:nodeInfo 48 cpu_id_t index; local 50 : [result] "=r"(index) 51 : [offset] "i"(OFFSETOF(nodeInfo_t, index))); 52 return index;
|
/seL4-l4v-master/l4v/misc/filemerge/faster/ |
H A D | translate.cpp | 50 unsigned int index = 0; local 55 buffer[index++] = c; 57 if ((index == 1 && buffer[0] != '\\') || 58 (index == 2 && buffer[1] != '<') || 59 (index == 3 && buffer[2] == '^')) { 61 buffer[index] = '\0'; 63 index = 0; 64 } else if (buffer[index - 1] == '>') { 65 buffer[index] = '\0'; 68 die("unrecognised ASCII sequence \"%.*ls\"", (int)index, 114 int index = 0; local [all...] |
/seL4-l4v-master/seL4/src/plat/imx31/machine/ |
H A D | hardware.c | 92 word_t index; local 94 for (index = L2_LINE_INDEX(start); 95 index < L2_LINE_INDEX(end) + 1; 96 index++) { 97 line = index << L2_LINE_SIZE_BITS; 106 word_t index; local 108 for (index = L2_LINE_INDEX(start); 109 index < L2_LINE_INDEX(end) + 1; 110 index++) { 111 line = index << L2_LINE_SIZE_BIT 121 word_t index; local [all...] |
/seL4-l4v-master/HOL4/examples/zipper/ |
H A D | zipperScript.sml | 16 val index_def = Define`index (Z p a s) = LENGTH p` 21 ``index z < size z``, 51 ``index (moveLeft z) = if 0 < index z then index z - 1 else 0``, 57 ``0 < index z ��� index (moveLeft z) = index z - 1``, 62 ``0 < index z ==> moveLeft z <> z``, 68 ``index [all...] |
/seL4-l4v-master/HOL4/src/unwind/Manual/ |
H A D | Makefile | 30 entries.tex index.tex \ 34 @echo "\begin{theindex}" > index.tex 35 @echo "\mbox{}" >> index.tex 36 @echo "\end{theindex}" >> index.tex 44 index: 45 ${MAKEINDEX} unwind.idx index.tex 57 make clean; make tex; make unwind; make index; make unwind ps pdf
|
/seL4-l4v-master/seL4/include/arch/arm/arch/model/ |
H A D | smp.h | 14 static inline cpu_id_t cpuIndexToID(word_t index) argument 16 return BIT(index);
|
/seL4-l4v-master/seL4/libsel4/include/sel4/ |
H A D | macros.h | 50 #define SEL4_SIZE_SANITY(index, entry, size) SEL4_COMPILE_ASSERT(index##entry##size, index + entry == size)
|
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
H A D | appendix0.tex | 11 \texttt{[|}\index{$Isabrl@\ttlbr|bold} & 14 \texttt{|]}\index{$Isabrr@\ttrbr|bold} & 19 \isasymAnd\index{$IsaAnd@\isasymAnd|bold}& 20 \texttt{!!}\index{$IsaAnd@\ttAnd|bold} & 44 \texttt{|}\index{$HOL0or@\ttor|bold} & 50 \verb$~$\index{$HOL0not@\verb$~$|bold} & 53 \verb$~=$\index{$HOL0noteq@\verb$~=$|bold} & 56 \ttindexbold{ALL}, \texttt{!}\index{$HOL0All@\ttall|bold} & 59 \ttindexbold{EX}, \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} & 61 \isasymuniqex\index{ [all...] |
H A D | root.tex | 15 \index{conditional expressions|see{\isa{if} expressions}} 16 \index{primitive recursion|see{recursion, primitive}} 17 \index{product type|see{pairs and tuples}} 18 \index{structural induction|see{induction, structural}} 19 \index{termination|see{functions, total}} 20 \index{tuples|see{pairs and tuples}} 21 \index{*<*lex*>|see{lexicographic product}}
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | appendix0.tex | 11 \texttt{[|}\index{$Isabrl@\ttlbr|bold} & 14 \texttt{|]}\index{$Isabrr@\ttrbr|bold} & 19 \isasymAnd\index{$IsaAnd@\isasymAnd|bold}& 20 \texttt{!!}\index{$IsaAnd@\ttAnd|bold} & 44 \texttt{|}\index{$HOL0or@\ttor|bold} & 50 \verb$~$\index{$HOL0not@\verb$~$|bold} & 53 \verb$~=$\index{$HOL0noteq@\verb$~=$|bold} & 56 \ttindexbold{ALL}, \texttt{!}\index{$HOL0All@\ttall|bold} & 59 \ttindexbold{EX}, \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} & 61 \isasymuniqex\index{ [all...] |
H A D | root.tex | 15 \index{conditional expressions|see{\isa{if} expressions}} 16 \index{primitive recursion|see{recursion, primitive}} 17 \index{product type|see{pairs and tuples}} 18 \index{structural induction|see{induction, structural}} 19 \index{termination|see{functions, total}} 20 \index{tuples|see{pairs and tuples}} 21 \index{*<*lex*>|see{lexicographic product}}
|
/seL4-l4v-master/isabelle/src/Doc/How_to_Prove_it/document/ |
H A D | prelude.tex | 1 \usepackage{makeidx} % allows index generation 4 \usepackage{multicol} % used for the two-column index 34 {\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}} 55 %index 57 \newcommand{\concept}[1]{\conceptnoidx{#1}\index{#1}} 58 \newcommand{\conceptidx}[2]{\conceptnoidx{#1}\index{#2}} 59 \newcommand{\indexed}[2]{#1\index{#2@\protect#1}}
|
/seL4-l4v-master/l4v/isabelle/src/Doc/How_to_Prove_it/document/ |
H A D | prelude.tex | 1 \usepackage{makeidx} % allows index generation 4 \usepackage{multicol} % used for the two-column index 34 {\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}} 55 %index 57 \newcommand{\concept}[1]{\conceptnoidx{#1}\index{#1}} 58 \newcommand{\conceptidx}[2]{\conceptnoidx{#1}\index{#2}} 59 \newcommand{\indexed}[2]{#1\index{#2@\protect#1}}
|
/seL4-l4v-master/l4v/tools/c-parser/testfiles/ |
H A D | extern_dups.c | 25 int index(int i) function
|
/seL4-l4v-master/seL4/src/plat/pc99/machine/ |
H A D | ioapic.c | 89 int index = ioapic * IOAPIC_IRQ_LINES + pin; local 95 ioredtbl_state[index] |= IOREDTBL_LOW_INTERRUPT_MASK; 97 ioredtbl_state[index] &= ~IOREDTBL_LOW_INTERRUPT_MASK; 100 assert((ioredtbl_state[index] & 0xff) != 0); 103 ioapic_write(ioapic, IOAPIC_WINDOW, ioredtbl_state[index]); 150 uint32_t index = 0; local 152 index = ioapic * IOAPIC_IRQ_LINES + pin; 159 ioredtbl_state[index] = IOREDTBL_LOW_INTERRUPT_MASK | 166 ioredtbl_state[index] |= ioapic_read(ioapic, IOAPIC_WINDOW) & ~MASK(16); 167 ioapic_write(ioapic, IOAPIC_WINDOW, ioredtbl_state[index]); [all...] |
/seL4-l4v-master/HOL4/src/num/arith/Manual/ |
H A D | description.tex | 6 arithmetic\index{linear arithmetic}. There are also some associated functions, 11 Presburger natural arithmetic\index{Presburger arithmetic}. Presburger natural 17 Products\index{products}\index{multiplication} of two expressions which both 23 been put in prenex normal form\index{prenex normal form} it must contain only 25 universal\index{quantifiers!universal} (`forall') or all 26 existential\index{quantifiers!existential}. Variables may appear 27 free\index{free variables} (unquantified) provided any quantifiers that do 32 \index{normalisation} 33 The function makes use of a number of preprocessors\index{preprocessor [all...] |
H A D | Makefile | 36 index: 49 make clean; make tex; make arith; make index; make arith ps pdf
|
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | Symbol.sml | 6 val index : symbol -> int value 35 fun mkSymbol name index = 36 (name,index) : symbol 39 fun index(s,n) = n function
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | Symbol.sml | 6 val index : symbol -> int value 35 fun mkSymbol name index = 36 (name,index) : symbol 39 fun index(s,n) = n function
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | Symbol.sml | 6 val index : symbol -> int value 35 fun mkSymbol name index = 36 (name,index) : symbol 39 fun index(s,n) = n function
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | Symbol.sml | 6 val index : symbol -> int value 35 fun mkSymbol name index = 36 (name,index) : symbol 39 fun index(s,n) = n function
|
/seL4-l4v-master/HOL4/src/num/reduce/Manual/ |
H A D | Makefile | 13 all:; make clean; make ids; make reduce; make index; make reduce ps pdf 23 index:
|