• 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
      • Booting-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • X86isa-state
        • Syscalls
          • Syscalls-logic
          • X86-syscall-args-and-return-value-marshalling
          • Syscall-numbers
          • Syscalls-exec
        • Cpuid
        • Linear-memory
        • Rflag-specifications
        • Characterizing-undefined-behavior
        • Top-level-memory
        • App-view
        • X86-decoder
        • Physical-memory
        • Decoding-and-spec-utils
        • Instructions
        • Register-readers-and-writers
        • X86-modes
        • Segmentation
        • Other-non-deterministic-computations
        • Environment
        • Paging
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Syscalls

Syscalls-exec

Syscall definitions to be used in the application-level view for execution

The definitions of the following (not inlined) functions in ACL2 have been smashed in raw Lisp; see the book environment-and-syscalls-raw.lsp for the raw Lisp definitions. These raw Lisp definitions are used when doing execution, and the ACL2 definitions are used when reasoning.

IMPORTANT: The following raw Lisp definitions will not be available unless the x86 books have been build with the environment variable X86ISA_EXEC set to t. See x86isa-build-instructions for details.

• env-read
• env-write
• read-x86-file-des
• read-x86-file-contents
• write-x86-file-des
• delete-x86-file-des
• write-x86-file-contents
• delete-x86-file-contents
• pop-x86-oracle
• syscall-read
• syscall-write
• syscall-open
• syscall-close
• syscall-lseek
• syscall-fadvise64
• syscall-link
• syscall-unlink
• syscall-dup
• syscall-dup2
• syscall-fcntl
• syscall-truncate
• syscall-ftruncate
• syscall-stat
• syscall-fstat
• syscall-lstat