Major Section: ACL2-BUILT-INS
(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. 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 and the returned state has the updated (popped)
acl2-oracle.
Example: (getenv$ "PWD" state) ==> (mv nil "/u/joe/work" state)Also see setenv$.
