• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
        • Io
        • Defttag
        • Sys-call
          • Sys-call+
          • Tshell
          • Sys-call-status
          • Sys-call*
          • Save-exec
          • Quicklisp
          • Std/io
          • Oslib
          • Bridge
          • Clex
          • Tshell
          • Unsound-eval
          • Hacker
          • ACL2s-interface
          • Startup-banner
          • Command-line
      • Interfacing-tools
        • Io
        • Defttag
        • Sys-call
          • Sys-call+
          • Tshell
          • Sys-call-status
          • Sys-call*
          • Save-exec
          • Quicklisp
          • Std/io
          • Oslib
          • Bridge
          • Clex
          • Tshell
          • Unsound-eval
          • Hacker
          • ACL2s-interface
          • Startup-banner
          • Command-line
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Sys-call
      • ACL2-built-ins

      Sys-call*

      Make a system call to the host OS, returning a status

      See sys-call+ for a closely related utility. There are only the following two differences between sys-call* and sys-call+.

      • Both return an error-triple (mv erp val state), but for sys-call*, val is always nil after printing as a side effect like sys-call. (For sys-call+, val is the string produced as output by the command.)
      • Logically, sys-call* pops the oracle once, not twice.