make a system call to the host OS, returning status and output
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.)

Erp is either nil or a non-zero integer. Normally, nil indicates that the command ran without error, and otherwise erp is the exit status.

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 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.