Major Section: ACL2-BUILT-INS
Example Form:
; The following returns (mv nil s state), where s is the standard output
; from the command: ls -l ./
(sys-call+ "ls" '("-l" "./") state)
General Form:
(sys-call+ cmd args state)
where cmd is a command to the host operating system and args is a
list of strings. Also see sys-call; but there are two differences between
sys-call and sys-call+. First, the latter takes an extra argument,
state. Second, while sys-call returns nil, sys-call+ returns
three values: a so-called error triple (see error-triples),
(mv erp val state). While execution returns values as described just
below, further below we explain the logical return values. In the following,
please keep in mind that the exact behavior depends on the platform; the
description is only a guide. For example, on some platforms erp might
always be nil, even if in the error case, and val might or might not
include error output. (For details, look at the ACL2 source code for
function system-call+, whose output is converted by replacing an erp
of nil by 0.)
Erpis eithernilor a non-zero integer. Normally,nilindicates that the command ran without error, and otherwiseerpis the exit status.
Valis a string, typically the output generated by the call ofcmd.
Stateis an ACL2 state.
While the description above pertains to the values returned by executing
sys-call+, the logical values are as follows. For a discussion of the
acl2-oracle field of an ACL2 state, see state.
Erpis the first element of theacl2-oracleof the input state if that element is a nonzero integer, and otherwise isnil.
Valis the second element of theacl2-oracleof the input state if it is a string, else the empty string,"".
Stateis the result of popping theacl2-oraclefield twice from the input state.
Note that unlike sys-call, a call of sys-call+ has no effect on
subsequent calls of sys-call-status.
As is the case for sys-call, a trust tag is required to call
sys-call+. For discussion of this and more, see sys-call.
