Searched refs:original (Results 1 - 6 of 6) sorted by relevance

/seL4-mcs-10.1.1/src/arch/x86/machine/
H A Dcpu_identification.c62 struct family_model original)
70 if (original.family != 0x0F) {
71 ci->display.family = original.family;
73 ci->display.family = ci->display.extended_family + original.family;
77 * original family_ID value read from CPUID.EAX, like:
78 * if (original->family == 0x06 || original->family == 0x0F) {
96 ci->display.model = (ci->display.extended_model << 4u) + original.model;
98 ci->display.model = original.model;
104 struct family_model original)
61 x86_cpuid_intel_identity_initialize(cpu_identity_t *ci, struct family_model original) argument
103 x86_cpuid_amd_identity_initialize(cpu_identity_t *ci, struct family_model original) argument
126 struct family_model original; local
[all...]
/seL4-mcs-10.1.1/manual/parts/
H A Dcspace.tex86 the original and a different guard (see
92 capability has the same badge and guard as the original.
100 original copy remaining.
150 capabilities may be manufactured from this original capability, using
179 only \emph{original} capabilities support derivation invocations, but
218 are the original capability to the respective object, both are
221 Ordinary original capabilities can have one level of derived
226 The original \obj{Endpoint} or \emph{Notification} capability will be unbadged. Using
229 an original capability (the ``original badge
[all...]
H A Dobjects.tex90 original capability (never with more rights). A newly minted
95 been derived from the original capability being revoked. The propagation of
172 giving the receiver the right to reply to the original sender. The reply
334 the original untyped memory object.
402 By calling \apifunc{seL4\_CNode\_Revoke}{cnode_revoke} on the original capability to an untyped memory
H A Dipc.tex155 A received capability has the same rights as the original, except if
H A Dthreads.tex628 A \obj{TCB} with a bound \obj{VCPU} has two execution modes; one is the original thread just as
/seL4-mcs-10.1.1/src/arch/x86/object/
H A Dvcpu.c406 applyFixedBits(uint32_t original, uint32_t high, uint32_t low) argument
408 original |= high;
409 original &= low;
410 return original;

Completed in 59 milliseconds