		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-computation-states

Var-autop

Check if a variable is found in automatic storage.

Signature
(var-autop var compst) → yes/no
Arguments: var — Guard (identp var).; compst — Guard (compustatep compst).
Returns: yes/no — Type (booleanp yes/no).

This checks whether the variable is in the scopes of the top frame. Thus, it only looks in the currently accessible (by variable names) automatic storage; it does not look in other frames.

This predicate serves to establish, when negated, that a variable is found in static storage, and not in automatic storage. Rules for this process are given later.

Definitions and Theorems

Function: var-autop

(defun var-autop (var compst)
  (declare (xargs :guard (and (identp var)
                              (compustatep compst))))
  (declare (xargs :guard (> (compustate-frames-number compst)
                            0)))
  (let ((__function__ 'var-autop))
    (declare (ignorable __function__))
    (var-in-scopes-p var
                     (frame->scopes (top-frame compst)))))

Theorem: booleanp-of-var-autop

(defthm booleanp-of-var-autop
  (b* ((yes/no (var-autop var compst)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: var-autop-of-ident-fix-var

(defthm var-autop-of-ident-fix-var
  (equal (var-autop (ident-fix var) compst)
         (var-autop var compst)))

Theorem: var-autop-ident-equiv-congruence-on-var

(defthm var-autop-ident-equiv-congruence-on-var
  (implies (ident-equiv var var-equiv)
           (equal (var-autop var compst)
                  (var-autop var-equiv compst)))
  :rule-classes :congruence)

Theorem: var-autop-of-compustate-fix-compst

(defthm var-autop-of-compustate-fix-compst
  (equal (var-autop var (compustate-fix compst))
         (var-autop var compst)))

Theorem: var-autop-compustate-equiv-congruence-on-compst

(defthm var-autop-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (var-autop var compst)
                  (var-autop var compst-equiv)))
  :rule-classes :congruence)