Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
X86isa
Program-execution
Introduction
X86isa-build-instructions
Publications
Contributors
Machine
Syscalls
Cpuid
X86isa-state
Linear-memory
Rflag-specifications
Characterizing-undefined-behavior
Top-level-memory
App-view
X86-decoder
Physical-memory
Decoding-and-spec-utils
Instructions
X86-modes
Register-readers-and-writers
Segmentation
Ea-to-la
Segment-base-and-bounds
Ia32e-segmentation
Make-system-segment-attr-field
Make-data-segment-attr-field
Make-code-segment-attr-field
Ia32e-valid-code-segment-descriptor-p
Ia32e-valid-busy-tss-segment-descriptor-p
Ia32e-valid-available-tss-segment-descriptor-p
Ia32e-valid-trap-gates-segment-descriptor-p
Ia32e-valid-ldt-segment-descriptor-p
Ia32e-valid-interrupt-gates-segment-descriptor-p
Ia32e-valid-data-segment-descriptor-p
Ia32e-valid-call-gate-segment-descriptor-p
Eas-to-las
Ia32-segmentation
Other-non-deterministic-computations
Environment
Paging
Implemented-opcodes
Proof-utilities
To-do
Concrete-simulation-examples
Model-validation
Utils
Debugging-code-proofs
Axe
Execloader
Math
Testing-utilities
Segmentation
Ia32e-segmentation
Specification of Segmentation in 64-bit Mode
Subtopics
Make-system-segment-attr-field
Constructor for the System Segment attribute field
Make-data-segment-attr-field
Constructor for the Data Segment attribute field
Make-code-segment-attr-field
Constructor for the Code Segment attribute field
Ia32e-valid-code-segment-descriptor-p
Recognizer for a valid code segment descriptor in 64-bit mode
Ia32e-valid-busy-tss-segment-descriptor-p
Recognizer for a valid Busy TSS segment descriptor
Ia32e-valid-available-tss-segment-descriptor-p
Recognizer for a valid Available TSS segment descriptor
Ia32e-valid-trap-gates-segment-descriptor-p
Recognizer for a valid Trap Gate segment descriptor
Ia32e-valid-ldt-segment-descriptor-p
Recognizer for a valid LDT segment descriptor
Ia32e-valid-interrupt-gates-segment-descriptor-p
Recognizer for a valid Interrupt Gate segment descriptor
Ia32e-valid-data-segment-descriptor-p
Recognizer for a valid data segment descriptor
Ia32e-valid-call-gate-segment-descriptor-p
Recognizer for a valid Call Gate segment descriptor