A | |
| address [X86Types] |
The memory address format supported by the machine language
|
| arith_op [X86Types] |
Arithmetic operations
|
B | |
| bits [AsmUtil] |
A bit source to use with functional IO
|
| bvector [CoqBvector] | |
C | |
| cc [X86Types] |
A condition code is a pair of a basic condition and a boolean indicating
whether that condition is true.
|
| condition [X86Types] |
Basic conditions
|
| control_reg [X86Types] |
Control registers
|
D | |
| debug_reg [X86Types] |
Debug registers
|
E | |
| env [Accel_ocaml] | |
F | |
| flag [X86Types] |
Flags
|
| float_reg [X86Types] |
Floating-point registers
|
G | |
| genop [X86Types] |
Generic instruction operands, indexed by the relevant register set
|
| genop32 [X86Types] | |
| genop8 [X86Types] |
Specializations to particular register sets
|
I | |
| inductive_info [Accel_ocaml_custom] | |
| inductive_name [Accel_ocaml_custom] | |
| instr [X86Types] |
The actual instructions.
|
M | |
| mmx_reg [X86Types] |
MMX registers
|
N | |
| nat [CoqNat] | |
P | |
| printer [X86Print] |
The type of a method for printing an
'a
|
| prod [X86Types] |
A normal type for pairs, since Coq extraction can't seem to produce code
that uses built-in tuple types.
|
R | |
| reg16 [X86Types] |
General-purpose 16-bit registers
|
| reg32 [X86Types] |
General-purpose 32-bit registers
|
| reg8 [X86Types] |
General-purpose 8-bit registers
|
S | |
| scale [X86Types] |
Scales for integer operations
|
| segment_reg [X86Types] |
Segment registers
|
| shift_op [X86Types] |
Bitwise shift operations
|
| sse [X86Types] |
SSE tests
|
T | |
| test_reg [X86Types] |
Test registers
|
Z | |
| z [CoqZ] |