• Top
    • Documentation
      • Xdoc
        • Missing-parents
          • Exec-bgeu
          • Exec-bltu
          • Exec-blt
          • Exec-bge
          • Exec-jalr
          • Exec-bne
          • Exec-beq
          • Exec-sra
          • Exec-op-imms-32
          • Exec-srl
          • Exec-sll
          • Exec-op-imms64
          • Exec-op-imms32
          • Exec-op-imm-32
          • Exec-op-32
          • Exec-op
          • Exec-branch
          • Exec-srlw
          • Exec-srliw
          • Exec-sraw
          • Exec-sraiw
          • Exec-sltiu
          • Exec-remuw
          • Exec-op-imm
          • Exec-jal
          • Exec-store
          • Exec-srli64
          • Exec-srli32
          • Exec-srai64
          • Exec-srai32
          • Exec-sllw
          • Exec-remw
          • Exec-load
          • Exec-divuw
          • Exec-addiw
          • Exec-xori
          • Exec-slti
          • Exec-slliw
          • Exec-remu
          • Exec-rem
          • Exec-divw
          • Exec-sw
          • Exec-slli64
          • Exec-slli32
          • Exec-ori
          • Exec-mulhsu
          • Exec-divu
          • Exec-andi
          • Exec-addi
          • Exec-sltu
          • Exec-slt
          • Exec-mulhu
          • Exec-lwu
          • Exec-div
          • Exec-auipc
          • Exec-addw
          • Exec-xor
          • Exec-mulw
          • Exec-mulh
          • Exec-and
          • Exec-subw
          • Exec-sub
          • Exec-sh
          • Exec-sd
          • Exec-sb
          • Exec-or
          • Exec-lhu
          • Exec-lh
          • Exec-ld
          • Exec-lbu
          • Exec-lb
          • Exec-mul
          • Exec-add
          • Exec-lw
          • Exec-lui
          • Eff-addr
          • Exec-instr
          • Missing-parents-test
        • Undocumented
        • Save
        • Defsection
        • Markup
        • Preprocessor
        • Terminal
        • Emacs-links
        • Defxdoc
        • Katex-integration
        • Constructors
        • Entities
        • Defxdoc+
        • Save-rendered
        • Add-resource-directory
        • Testing
        • Order-subtopics
        • Save-rendered-event
        • Archive-matching-topics
        • Archive-xdoc
        • Xdoc-extend
        • Set-default-parents
        • Defpointer
        • Defxdoc-raw
        • Xdoc-tests
        • Xdoc-prepend
        • Defsection-progn
        • Gen-xdoc-for-file
      • ACL2-doc
      • Recursion-and-induction
      • Loop$-primer
      • Operational-semantics
      • Pointers
      • Doc
      • Documentation-copyright
      • Course-materials
      • Publications
      • Args
      • ACL2-doc-summary
      • Finding-documentation
      • Broken-link
      • Doc-terminal-test-2
      • Doc-terminal-test-1
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Xdoc

Missing-parents

Placeholder for documentation topics that lack :parents.

If a defxdoc form ends up having no parents, it ends up being put here. See also undocumented.

Historic note. We used to put these topics directly underneath top instead. But we found that during development, this sometimes led to a strange-looking hierarchy where ``random'' topics were presented as top-level topics just because they were new or being moved around or because set-default-parents forms weren't quite in the right places. To avoid this, we now move these topics to missing-parents and print notes about them when a manual is saved with save.

Subtopics

Exec-bgeu
Semantics of the BGEU instruction [ISA:2.5.2].
Exec-bltu
Semantics of the BLTU instruction [ISA:2.5.2].
Exec-blt
Semantics of the BLT instruction [ISA:2.5.2].
Exec-bge
Semantics of the BGE instruction [ISA:2.5.2].
Exec-jalr
Semantics of the JALR instruction [ISA:2.5.1].
Exec-bne
Semantics of the BNE instruction [ISA:2.5.2].
Exec-beq
Semantics of the BEQ instruction [ISA:2.5.2].
Exec-sra
Semantics of the SRA instruction [ISA:4.2.2].
Exec-op-imms-32
Semantics of a shift instruction with the OP-IMM-32 opcode [ISA:4.2.1].
Exec-srl
Semantics of the SRL instruction [ISA:4.2.2].
Exec-sll
Semantics of the SLL instruction [ISA:4.2.2].
Exec-op-imms64
Semantics of the shift instructions with the OP-IMM opcode [ISA:2.4.1] in 64-bit mode.
Exec-op-imms32
Semantics of the shift instructions with the OP-IMM opcode [ISA:2.4.1] in 32-bit mode.
Exec-op-imm-32
Semantics of the non-shift instructions with the OP-IMM-32 opcode [ISA:4.2.1].
Exec-op-32
Semantics of the instructions with the OP-32 opcode [ISA:4.2.2] [ISA:13.1] [ISA:13.2].
Exec-op
Semantics of the instructions with the OP opcode [ISA:2.4.2] [ISA:4.2.2] [ISA:13.1] [ISA:13.2].
Exec-branch
Semantics of the instructions with the BRANCH opcode [ISA:2.5.2].
Exec-srlw
Semantics of the SRLW instruction [ISA:4.2.2].
Exec-srliw
Semantics of the SRLIW instruction [ISA:4.2.1].
Exec-sraw
Semantics of the SRAW instruction [ISA:4.2.2].
Exec-sraiw
Semantics of the SRAIW instruction [ISA:4.2.1].
Exec-sltiu
Semantics of the SLTIU instruction [ISA:2.4.1].
Exec-remuw
Semantics of the REMUW instruction [ISA:13.2].
Exec-op-imm
Semantics of the non-shift instructions with the OP-IMM opcode [ISA:2.4.1].
Exec-jal
Semantics of the JAL instruction [ISA:2.5.1].
Exec-store
Semantics of the instructions with the STORE opcode [ISA:2.6].
Exec-srli64
Semantics of the SRLI instruction [ISA:2.4.1] in 64-bit mode.
Exec-srli32
Semantics of the SRLI instruction [ISA:2.4.1] in 32-bit mode.
Exec-srai64
Semantics of the SRAI instruction [ISA:2.4.1] in 64-bit mode.
Exec-srai32
Semantics of the SRAI instruction [ISA:2.4.1] in 32-bit mode.
Exec-sllw
Semantics of the SLLW instruction [ISA:4.2.2].
Exec-remw
Semantics of the REMW instruction [ISA:13.2].
Exec-load
Semantics of the instructions with the LOAD opcode [ISA:2.6].
Exec-divuw
Semantics of the DIVUW instruction [ISA:13.2].
Exec-addiw
Semantics of the ADDIW instruction [ISA:4.2.1].
Exec-xori
Semantics of the XORI instruction [ISA:2.4.1].
Exec-slti
Semantics of the SLTI instruction [ISA:2.4.1].
Exec-slliw
Semantics of the SLLIW instruction [ISA:4.2.1].
Exec-remu
Semanics of the REMU instruction [ISA:13.2].
Exec-rem
Semanics of the REM instruction [ISA:13.2].
Exec-divw
Semantics of the DIVW instruction [ISA:13.2].
Exec-sw
Semantics of the SW instruction [ISA:2.6].
Exec-slli64
Semantics of the SLLI instruction [ISA:2.4.1] in 64-bit mode.
Exec-slli32
Semantics of the SLLI instruction [ISA:2.4.1] in 32-bit mode.
Exec-ori
Semantics of the ORI instruction [ISA:2.4.1].
Exec-mulhsu
Semanics of the MULHSU instruction [ISA:13.1].
Exec-divu
Semanics of the DIVU instruction [ISA:13.2].
Exec-andi
Semantics of the ANDI instruction [ISA:2.4.1].
Exec-addi
Semantics of the ADDI instruction [ISA:2.4.1].
Exec-sltu
Semantics of the SLTU instruction [ISA:2.4.2].
Exec-slt
Semantics of the SLT instruction [ISA:2.4.2].
Exec-mulhu
Semanics of the MULHU instruction [ISA:13.1].
Exec-lwu
Semantics of the LW instruction [ISA:4.3].
Exec-div
Semanics of the DIV instruction [ISA:13.2].
Exec-auipc
Semantics of the AUIPC instruction [ISA:4.2.1].
Exec-addw
Semantics of the ADDW instruction [ISA:4.2.2].
Exec-xor
Semantics of the XOR instruction [ISA:2.4.2].
Exec-mulw
Semantics of the MULW instruction [ISA:13.1].
Exec-mulh
Semanics of the MULH instruction [ISA:13.1].
Exec-and
Semantics of the AND instruction [ISA:2.4.2].
Exec-subw
Semantics of the SUBW instruction [ISA:4.2.2].
Exec-sub
Semantics of the SUB instruction [ISA:2.4.2].
Exec-sh
Semantics of the SH instruction [ISA:2.6].
Exec-sd
Semantics of the SD instruction [ISA:4.3].
Exec-sb
Semantics of the SB instruction [ISA:2.6].
Exec-or
Semantics of the OR instruction [ISA:2.4.2].
Exec-lhu
Semantics of the LHU instruction [ISA:2.6].
Exec-lh
Semantics of the LH instruction [ISA:2.6].
Exec-ld
Semantics of the LW instruction [ISA:4.3].
Exec-lbu
Semantics of the LBU instruction [ISA:2.6].
Exec-lb
Semantics of the LB instruction [ISA:2.6].
Exec-mul
Semanics of the MUL instruction [ISA:13.1].
Exec-add
Semantics of the ADD instruction [ISA:2.4.2].
Exec-lw
Semantics of the LW instruction [ISA:2.6].
Exec-lui
Semantics of the LUI instruction [ISA:4.2.1].
Eff-addr
Effective address for a load or store instruction [ISA:2.6].
Exec-instr
Semantics of instructions.
Missing-parents-test
A topic with no :parents.