/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | poly_specific.cpp | 312 byte *pointer; local 316 pointer = closure.AsCodePtr(); 317 else pointer = *(POLYCODEPTR*)(closure.AsObjPtr()); 318 // pointer is the start of the code segment. 321 pointer += offset.UnTaggedUnsigned(); 322 byte* writeable = gMem.SpaceForAddress(pointer)->writeAble(pointer); 354 size_t c = target - pointer - 4; 364 // it is an absolute address rather than an object pointer. 369 pointer[ 381 byte *pointer = *(POLYCODEPTR*)(closure.AsObjPtr()); local 389 byte *pointer = *(POLYCODEPTR*)(closure.AsObjPtr()); local [all...] |
H A D | x86assembly_masm32.S | 26 ; edx: Closure pointer in call. 30 ; esp: Stack pointer. 50 SaveCStack DWORD ? ; Saved C stack pointer 52 StackPtr DWORD ? ; Stack pointer 116 mov [ArgVector.StackPtr+ebp],esp ; Save ML stack pointer 117 mov esp,[ArgVector.SaveCStack+ebp] ; Restore C stack pointer
|
H A D | x86assembly_masm64.S | 26 ; rdx: Closure pointer in call. 30 ; rsp: Stack pointer. 38 ; r15: Memory allocation pointer 59 StackPtr QWORD ? ; Stack pointer 123 mov [ArgVector.SaveCStack+rcx],rsp ; Save the C stack pointer 181 mov [ArgVector.StackPtr+rbp],rsp ; Save ML stack pointer 182 mov [ArgVector.LocalMpointer+rbp],r15 ; Save back heap pointer 183 mov rsp,[ArgVector.SaveCStack+rbp] ; Restore C stack pointer
|
H A D | x86assembly_gas32.S | 32 %%edx: Closure pointer in call. 36 %%esp: Stack pointer. 74 #define Arg_SaveCStack 0x18 /* Save C Stack pointer */ 137 movl %esp,Arg_StackPtr(%ebp) # Save ML stack pointer 138 movl Arg_SaveCStack(%ebp),%esp # Restore C stack pointer
|
H A D | x86assembly_gas64.S | 32 %rdx: Closure pointer in call. 36 %rsp: Stack pointer. 44 %r15: Memory allocation pointer 216 movq %r15,Arg_LocalMpointer(%rbp) # Save back heap pointer 217 movq Arg_SaveCStack(%rbp),%rsp # Restore C stack pointer
|
/seL4-l4v-master/seL4/src/arch/x86/32/ |
H A D | machine_asm.S | 30 lgdt (%eax) # load gdtr register with gdt pointer
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | PackRealBig.sml | 75 (* r is actually represented by a pointer to a vector. *) 137 (* r is actually represented by a pointer to a vector. *) 153 (* r is actually represented by a pointer to a vector. *) 215 (* r is actually represented by a pointer to a vector. *)
|
H A D | Weak.sml | 22 they require pointer equality. A weak reference or array behaves just like 96 pointer to the token there will be no change to the state. If, though, it discards 97 the data associated with the resource and hence the pointer to the token the
|
H A D | BinIO.sml | 71 a pointer into the io table. *)
|
H A D | IntInf.sml | 81 else (* i is actually a pointer to a byte segment. *)
|
/seL4-l4v-master/seL4/src/arch/x86/64/ |
H A D | machine_asm.S | 76 lgdt (%rdi) # load gdtr with gdt pointer
|
/seL4-l4v-master/HOL4/examples/HolBdd/ |
H A D | Varmap.sml | 85 (* Test pointer equality of varmaps *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/ |
H A D | X86FOREIGNCALL.sml | 60 We use esi to hold the argument data pointer and edi to save the ML stack pointer 202 (* Set the stack pointer past the data on the stack. For Windows/64 add in a 32 byte save area *) 331 loadMemory(esp, ebp, memRegStackPtr, nativeWordOpSize) (* Restore the ML stack pointer. *) 571 (* Save the stack pointer. *) 573 loadMemory(esp, ebp, memRegCStackPtr, nativeWordOpSize) (* Load the saved C stack pointer. *) 597 loadMemory(esp, ebp, memRegStackPtr, nativeWordOpSize) (* Restore the ML stack pointer. *) 729 (* Save the ML stack pointer because we may have grown the stack. Switch to the C stack. *) 903 (* Save the stack pointer. *) 905 loadMemory(esp, ebp, memRegCStackPtr, nativeWordOpSize) (* Load the saved C stack pointer [all...] |
/seL4-l4v-master/seL4/manual/tools/libsel4_tools/ |
H A D | syscall_stub_gen.py | 94 pointer. 130 def pointer(self): member in class:Type 132 Return a new Type class representing a pointer to this 158 A pointer to a standard type. 172 def pointer(self): member in class:PointerType 428 params.append(param.type.pointer().render_parameter_name(param.name)) 431 params.append(param.type.pointer().render_parameter_name(param.name))
|
/seL4-l4v-master/seL4/libsel4/tools/ |
H A D | syscall_stub_gen.py | 94 pointer. 130 def pointer(self): member in class:Type 132 Return a new Type class representing a pointer to this 158 A pointer to a standard type. 172 def pointer(self): member in class:PointerType 428 params.append(param.type.pointer().render_parameter_name(param.name)) 431 params.append(param.type.pointer().render_parameter_name(param.name))
|
/seL4-l4v-master/HOL4/src/datatype/ |
H A D | selftest.sml | 208 val _ = Hol_datatype`pointer = pnil | pref of 'a` 209 val _ = Hol_datatype`failure = <| head : 'a pointer; tail : failure pointer |>`
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | CFLScript.sml | 26 (* post-call processing. Pointer register hp (heap pointer, i.e. r10), fp *) 27 (* (frame pointer), ip (intra-procedure register pointer), sp (stack pointer) *)
|
H A D | funCall.sml | 250 (* old pointer | 1 | *) 254 (* new pointer *) 286 (* pointer *)
|
/seL4-l4v-master/HOL4/examples/machine-code/just-in-time/ |
H A D | jit_codegenScript.sml | 44 r1 = pointer to generated code 45 r2 = pointer to byte code instr 46 r3 = pointer to start of byte code 47 r4 = pointer to start of generated code 50 r7 = pointer to initial stack 122 (* r6 - pointer to bytecode, r5 - address in generated code *)
|
/seL4-l4v-master/HOL4/Manual/Description/ |
H A D | HolBdd.tex | 655 The integer returned as the first component of the pair is a pointer 657 descriptors. This pointer points to the root node. Each node 801 following the low ({\t{false}}) or high ({\t{true}}) pointer, 961 first component is the \emph{destructor} (a function pointer) and the 962 second component is the \emph{data} (typicaly a pointer). When the 1072 \t{Varmap.eq} & pointer equality of varmaps ({\it not} general equality) \\ \hline 1427 pointer equal 1462 {\t{\footnotesize BddOpError}} is raised if the varmaps of the hypotheses are not pointer equal 1569 Raises \t{BddAppallError} if the varmaps in the hypotheses are not pointer equal, or 1612 Raises \t{BddAppexError} if the varmaps of the hypotheses are not pointer equa [all...] |
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
H A D | HolBdd.tex | 655 The integer returned as the first component of the pair is a pointer 657 descriptors. This pointer points to the root node. Each node 801 following the low ({\t{false}}) or high ({\t{true}}) pointer, 961 first component is the \emph{destructor} (a function pointer) and the 962 second component is the \emph{data} (typicaly a pointer). When the 1072 \t{Varmap.eq} & pointer equality of varmaps ({\it not} general equality) \\ \hline 1427 pointer equal 1462 {\t{\footnotesize BddOpError}} is raised if the varmaps of the hypotheses are not pointer equal 1569 Raises \t{BddAppallError} if the varmaps in the hypotheses are not pointer equal, or 1612 Raises \t{BddAppexError} if the varmaps of the hypotheses are not pointer equa [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw2/examples/ |
H A D | arm_compiler_demoScript.sml | 58 m5 - becomes memory location at address stack pointer + 5 485 rule of thumb. The option PushProcedure alters the stack pointer, and 486 hence what used to be at offset, say, 5 from the stack pointer (i.e. m5) 506 the stack pointer is shifted by one *) 537 The general case: PushProcedure (xs,i) will shift the stack pointer 549 PushProcedure (xs,i) shifts the stack pointer i steps, e.g. 556 It then alters the stack pointer to add two more elements:
|
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | funCall.sml | 265 (* old pointer | 1 | *) 269 (* new pointer *) 301 (* pointer *)
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | funCall.sml | 253 (* old pointer | 1 | *) 257 (* new pointer *) 289 (* pointer *)
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_equalScript.sml | 27 r15 - base pointer for "other" heap half 28 r0 - index pointer for "other" heap half
|