• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Debugging
    • Projects
    • 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
            • Two-byte-opcodes
            • One-byte-opcodes
            • Fp-opcodes
            • Instruction-semantic-functions
            • Opcode-maps
            • X86-illegal-instruction
            • Implemented-opcodes
            • X86-general-protection
            • X86-device-not-available
            • X86-step-unimplemented
            • Privileged-opcodes
              • X86-lldt
              • X86-lidt
              • X86-lgdt
          • X86-modes
          • Segmentation
          • Register-readers-and-writers
          • 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
  • Instructions

Privileged-opcodes

Instruction semantic functions for Intel's privileged instructions

Subtopics

X86-lldt
X86-lidt
X86-lgdt