Sys-call+
Make a system call to the host OS, returning status and output
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 related utilities sys-call and sys-call*. There are three major differences between sys-call and
both sys-call+ and sys-call*. First, the latter two take an extra
argument, state. Second, while sys-call returns nil,
sys-call+ and sys-call* both return an error-triple, (mv
erp val state). Finally, sys-call+ and sys-call* provide a
command to the host operating system even during a proof, which could be
useful in computed hints and clause processors. While execution returns
values as listed 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.)
Erp can be nil, indicating that after the command executes the
process status returned is 0, indicating a normal exit. Otherwise erp is
a non-zero integer, which is the status returned by the process when it
completes.
Val is a string, typically the output generated by the call of
cmd.
State is 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 read-ACL2-oracle and
state.
Erp is the first element of the acl2-oracle of the input state if
that element is a nonzero integer, and otherwise is nil.
Val is the second element of the acl2-oracle of the input state
if it is a string, else the empty string, "".
State is the result of popping the acl2-oracle field 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.
