• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
        • Program-execution
        • Sdm-instruction-set-summary
        • Tlb
        • Running-linux
        • Introduction
        • Asmtest
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
          • X86isa-state
          • Syscalls
          • Cpuid
          • Linear-memory
          • Rflag-specifications
          • Characterizing-undefined-behavior
          • Top-level-memory
          • App-view
          • X86-decoder
          • Physical-memory
          • Decoding-and-spec-utils
          • Instructions
          • Register-readers-and-writers
          • X86-modes
          • 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
        • To-do
        • Proof-utilities
        • Peripherals
        • Model-validation
        • Modelcalls
        • Concrete-simulation-examples
        • Utils
        • Debugging-code-proofs
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • 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