• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Running-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
        • Tty
          • Read-tty
          • Write-tty
          • Tty-bufferp
        • Timer
        • X86-exec-peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Tty

Tty-bufferp

Recognizer for the TTY buffers.

Signature

(tty-bufferp x) → *

tty-bufferp recognizes buffers which are valid as the tty-in and tty-out fields of the x86 stobj. These are true-listps which only contain 8-bit unsigned integers.

Definitions and Theorems

Function: tty-bufferp

(defun tty-bufferp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'tty-bufferp))
    (declare (ignorable __function__))
    (or (null x)
        (and (consp x)
             (unsigned-byte-p 8 (car x))
             (tty-bufferp (cdr x))))))