Searched refs:architecture (Results 1 - 25 of 39) sorted by relevance

12

/seL4-l4v-10.1.1/HOL4/polyml/
H A Dpolyexports.h72 unsigned architecture; // Machine architecture member in struct:_exportDescription
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/step/
H A Darm_configLib.sml3 For example: the architecture version, Thumb or ARM encoding, ...
120 val architecture = ``^st.Architecture`` value
141 [eq architecture (#arch),
/seL4-l4v-10.1.1/seL4/manual/parts/
H A Dvspace.tex17 each architecture defines its own objects for the top-level VSpace and further intermediate paging structures.
18 Common to every architecture is the \obj{Page}, representing a frame of physical memory.
32 Each architecture has a top-level paging structure (level 0) and a number of intermediate levels.
34 For each architecture, the VSpace is realised as a different object, as determined by the
58 The rest of this section details the paging structures for each architecture.
168 architecture and are documented in the \autoref{sec:api_reference} for each function.
170 At minimum, each architecture defines \texttt{Map}, \texttt{Unmap},\texttt{Remap} and
172 Methods for page objects for each architecture can be found in the \autoref{sec:api_reference}, and
173 are indexed per architecture in the table below.
183 Each architecture als
[all...]
H A Dbootup.tex114 Depending on the architecture and platform there might be additional pieces of boot
121 chunk that has no data, any other types are platform or architecture specific. The
156 contiguous, and is made up of the smallest frames available on the architecture.
158 available on the architecture it's running on.
H A Dthreads.tex22 or kernel object invocation that do not fit in the architecture-defined message
108 values that the architecture specifications have mandated to be certain values.
177 User exceptions are used to deliver architecture-defined exceptions. For
366 \obj{VCPU} objects also have additional, architecture specific, invocations for manipulating
372 the underlying architecture specific harwdare mechanisms is required to use these objects, and
H A Dipc.tex90 available on this architecture) then arguments 1 and 2 would be
/seL4-l4v-10.1.1/l4v/camkes/glue-spec/document/
H A Dintro.tex40 mechanisms that provide architecture and communication boundary enforcement.
57 constrained in their behaviour than the architecture boundaries enforce.
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/eval/
H A Demit_eval.sml91 fun architecture a = function
102 | _ => raise Fail "architecture"
632 mk_arm_state (architecture arch)
694 val _ = print "Enter architecture, initial register values and default\
H A Darm_evalLib.sml458 | SOME a => raise ERR "configure" ("not a valid architecture: " ^ a)
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DWord32In64.sml30 (* This version has been modified for 64-bit architecture and does not
H A DFinalPolyML.sml803 (* Construct suffixes with the architecture and version number in so
804 we can compile architecture- and version-specific code. *)
805 val archSuffix = "." ^ String.map Char.toLower (PolyML.architecture())
/seL4-l4v-10.1.1/l4v/spec/abstract/document/
H A Droot.tex145 seL4 microkernel on the \arch architecture.
/seL4-l4v-10.1.1/l4v/proof/bisim/document/
H A Droot.tex128 %seL4 microkernel on the ARMv6 architecture.
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Dpecoffexport.cpp352 exports.architecture = machineDependent->MachineArchitecture();
H A Delfexport.cpp272 # error "No support for exporting on this architecture"
411 ASSERT(0); // Wrong type of relocation for this architecture.
722 exports.architecture = machineDependent->MachineArchitecture();
H A Dmachoexport.cpp221 ASSERT(0); // Wrong type of relocation for this architecture.
294 #error "No support for exporting on this architecture"
484 exports.architecture = machineDependent->MachineArchitecture();
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DSmtLib_Logics.sml108 change to our parser architecture.
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/
H A Dx64AssemblerLib.sml2 Assembly code support for the x86-64 architecture specification
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A Darm_parserLib.sml799 arch_okay (s,"requires architecture with Thumb2 support") has_thumb2;
802 arch_okay (s,"requires architecture with DSP support") has_dsp;
805 arch_okay (s,"requires architecture version >= 5")
809 arch_okay (s,"requires architecture version >= 6")
813 arch_okay (s,"requires architecture version >= 7")
1980 arch_okay ("arm_parse_clrex", "not supported by architecture")
2949 arch_okay ("arm_parse_ldrexd", "not supported by selected architecture")
2970 arch_okay ("arm_parse_strexd", "not supported by selected architecture")
2995 "not supported by selected architecture")
3012 "not supported by selected architecture")
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/arm/
H A Dsysv.S64 @ This selects the minimum architecture level required.
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/model/
H A DarmAssemblerLib.sml2 Assembly code support for the ARMv7-AR architecture specification
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/model/
H A Dm0AssemblerLib.sml2 Assembly code support for the ARMv6-M architecture specification
/seL4-l4v-10.1.1/HOL4/tools-poly/
H A Dconfigure.sml207 (if PolyML.architecture() = "I386" then ["-arch", "i386"] else [])
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/src/
H A Driscv.spec84 -- Processor architecture
101 Architecture architecture(ab::arch_base) =
106 case _ => #UNDEFINED("Unknown architecture: " : [[ab] :: nat])
339 { 63-62 : ArchBase -- base architecture, machine mode on reset
748 architecture(MCSR.mcpuid.ArchBase)
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/
H A DarmScript.sml3 (* DESCRIPTION : Model of the ARM instruction set architecture (v4) *)

Completed in 339 milliseconds

12