Getenv$
Read an environment variable
(Getenv$ str state), where str is a string, reads the
value of environment variable str, returning a value of nil if none
is found or if the read fails. (Exception: if the value is not a legal ACL2
string, say because it contains a character with char-code exceeding
255, then an error is signaled.) The logical story is that getenv$
reads its value from the oracle field of the ACL2 state. The
return value is thus a triple of the form (mv erp val state), where
erp will always be nil in practice, and logically, val is the
top of the acl2-oracle field of the state (see read-ACL2-oracle) and
the returned state has the updated (popped) acl2-oracle.
Example:
(getenv$ "PWD" state) ==> (mv nil "/u/joe/work" state)
Also see setenv$.
Function: getenv$
(defun getenv$ (str state)
(declare (xargs :stobjs state
:guard (stringp str)))
(declare (ignore str))
(read-acl2-oracle state))
