• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
      • Defun
      • Declare
      • System-utilities
      • Stobj
      • State
        • World
        • Io
        • Wormhole
          • Wormhole-eval
          • Wormhole-implementation
          • Make-wormhole-status
          • Get-wormhole-status
          • Set-wormhole-entry-code
          • Set-wormhole-data
          • Wormhole-data
          • Wormhole-statusp
          • Wormhole-p
          • Wormhole-entry-code
        • Programming-with-state
        • W
        • Set-state-ok
        • Random$
      • Memoize
      • Mbe
      • Io
      • Apply$
      • Defpkg
      • Mutual-recursion
      • Loop$
      • Programming-with-state
      • Arrays
      • Characters
      • Time$
      • Loop$-primer
      • Fast-alists
      • Defmacro
      • Defconst
      • Evaluation
      • Guard
      • Equality-variants
      • Compilation
      • Hons
      • ACL2-built-ins
      • Developers-guide
      • System-attachments
      • Advanced-features
      • Set-check-invariant-risk
      • Numbers
      • Irrelevant-formals
      • Efficiency
      • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
      • Redefining-programs
      • Lists
      • Invariant-risk
      • Errors
      • Defabbrev
      • Conses
      • Alists
      • Set-register-invariant-risk
      • Strings
      • Program-wrapper
      • Get-internal-time
      • Basics
      • Packages
      • Defmacro-untouchable
      • Primitive
      • <<
      • Revert-world
      • Set-duplicate-keys-action
      • Unmemoize
      • Symbols
      • Def-list-constructor
      • Easy-simplify-term
      • Defiteration
      • Defopen
      • Sleep
    • Start-here
    • Real
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Wormhole

Get-wormhole-status

Make a wormhole's status visible outside the wormhole

General Form: (get-wormhole-status name state)

Name should be the name of a wormhole (see wormhole). This function returns an error-triple of the form (mv nil s state), where s is the status of the named wormhole. The status is obtained by reading the oracle in the ACL2 state.

This function makes the status of a wormhole visible outside the wormhole. But since this function takes state and modifies it, the function may only be used in contexts in which you may change state. Otherwise, the wormhole status may stay in the wormhole. See wormhole-eval and wormhole.