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
cmdis a command to the host operating system and
argsis a list of strings. Also see sys-call; but there are two differences between
sys-call+. First, the latter takes an extra argument,
state. Second, while
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
erpmight always be
nil, even if in the error case, and
valmight 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
nilor a non-zero integer. Normally,
nilindicates that the command ran without error, and otherwise
erpis the exit status.
Valis a string, typically the output generated by the call of
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 the
acl2-oracleof the input state if that element is a nonzero integer, and otherwise is
Valis the second element of the
acl2-oracleof the input state if it is a string, else the empty string,
Stateis the result of popping the
acl2-oraclefield twice from the input state.
Note that unlike
sys-call, a call of
sys-call+ has no effect on
subsequent calls of
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.