		Search-engine friendly clone of the ACL2 documentation.

Oslib

Getpid

Get the current process identification (PID) number.

Signature
(getpid &optional (state 'state)) → (mv pid new-state)
Returns: pid — The Process ID for this ACL2 session on success, or nil on failure.
Type (or (natp pid) (not pid)).; new-state — Type (state-p1 new-state), given (force (state-p1 state)).

This will just fail if called on an unsupported Lisp.

Definitions and Theorems

Function: getpid-fn

(defun getpid-fn (state)
       (declare (xargs :stobjs (state)))
       (declare (xargs :guard t))
       (let ((__function__ 'getpid))
            (declare (ignorable __function__))
            (b* ((- (raise "Raw Lisp definition not installed?"))
                 ((mv err val state)
                  (read-acl2-oracle state))
                 ((when err) (mv nil state)))
                (mv (nfix val) state))))

Theorem: return-type-of-getpid.pid

(defthm return-type-of-getpid.pid
        (b* (((mv ?pid ?new-state)
              (getpid-fn state)))
            (or (natp pid) (not pid)))
        :rule-classes :type-prescription)

Theorem: state-p1-of-getpid.new-state

(defthm state-p1-of-getpid.new-state
        (implies (force (state-p1 state))
                 (b* (((mv ?pid ?new-state)
                       (getpid-fn state)))
                     (state-p1 new-state)))
        :rule-classes :rewrite)

Theorem: w-state-of-getpid

(defthm w-state-of-getpid
        (b* (((mv ?pid ?new-state)
              (getpid-fn state)))
            (equal (w new-state) (w state))))