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
Implemented-opcodes
Proof-utilities
System-level-marking-view-proof-utilities
Rb-alt
Unwind-x86-interpreter-in-marking-view
Get-prefixes-alt
Get-prefixes-in-system-level-marking-view
Program-at-alt
Rb-in-system-level-marking-view
Xlate-equiv-memory-and-rml08
Reasoning-about-page-tables
Create-qword-address-list
Mult-8-qword-paddr-listp
Gather-paging-structures
Gather-all-paging-structure-qword-addresses
All-mem-except-paging-structures-equal
Gather-qword-addresses-corresponding-to-1-entry
Xlation-governing-entries-paddrs
Xlation-governing-entries-paddrs-for-page-dir-ptr-table
Xlate-equiv-structures
Xlation-governing-entries-paddrs-for-page-directory
All-xlation-governing-entries-paddrs
Xlation-governing-entries-paddrs-for-pml4-table
Gather-pml4-table-qword-addresses
Xlation-governing-entries-paddrs-for-page-table
Xlate-equiv-memory
Open-qword-paddr-list
Qword-paddr-listp
Find-l-addrs-from-disjoint-p$-of-two-las-to-pas-aux
Find-first-arg-of-disjoint-p$-candidates
Paging-basics
Las-to-pas-two-n-ind-hint
Find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux
Replace-element
Non-marking-view-proof-utilities
App-view-proof-utilities
Subset-p
Disjoint-p
Pos
Member-p
No-duplicates-p
Common-system-level-utils
Debugging-code-proofs
General-memory-utils
X86-row-wow-thms
To-do
Concrete-simulation-examples
Model-validation
Utils
Debugging-code-proofs
Axe
Execloader
Math
Testing-utilities
Reasoning-about-page-tables
Gather-paging-structures
Gather physical addresses where paging data structures are located
Subtopics
Gather-all-paging-structure-qword-addresses
Returns a list of qword addresses of all the active paging structures
All-mem-except-paging-structures-equal
Gather-qword-addresses-corresponding-to-1-entry
Xlation-governing-entries-paddrs
Xlation-governing-entries-paddrs-for-page-dir-ptr-table
Xlate-equiv-structures
Xlation-governing-entries-paddrs-for-page-directory
All-xlation-governing-entries-paddrs
Xlation-governing-entries-paddrs-for-pml4-table
Gather-pml4-table-qword-addresses
Xlation-governing-entries-paddrs-for-page-table
Xlate-equiv-memory
Open-qword-paddr-list