		Search-engine friendly clone of the ACL2 documentation.

Static-safety-checking

Check-safe-variable-single

Check if a single variable declaration is safe.

Signature
(check-safe-variable-single name init varset funtab) → varset?
Arguments: name — Guard (identifierp name).; init — Guard (expression-optionp init).; varset — Guard (identifier-setp varset).; funtab — Guard (funtablep funtab).
Returns: varset? — Type (identifier-set-resultp varset?).

This is used by check-safe-statement: see that function's documentation for background.

The name of the variable must be an identifier that is not already in the variable table. The expression is checked if present, and it must return exactly one result.

Definitions and Theorems

Function: check-safe-variable-single

(defun check-safe-variable-single (name init varset funtab)
  (declare (xargs :guard (and (identifierp name)
                              (expression-optionp init)
                              (identifier-setp varset)
                              (funtablep funtab))))
  (let ((__function__ 'check-safe-variable-single))
    (declare (ignorable __function__))
    (b* ((name (identifier-fix name))
         (init (expression-option-fix init))
         ((okf varset-new) (add-var name varset))
         ((when (not init)) varset-new)
         ((okf results)
          (check-safe-expression init varset funtab))
         ((unless (= results 1))
          (reserrf (list :declare-single-var-mismatch
                         name results))))
      varset-new)))

Theorem: identifier-set-resultp-of-check-safe-variable-single

(defthm identifier-set-resultp-of-check-safe-variable-single
  (b*
    ((varset? (check-safe-variable-single name init varset funtab)))
    (identifier-set-resultp varset?))
  :rule-classes :rewrite)

Theorem: check-safe-variable-single-of-identifier-fix-name

(defthm check-safe-variable-single-of-identifier-fix-name
  (equal (check-safe-variable-single (identifier-fix name)
                                     init varset funtab)
         (check-safe-variable-single name init varset funtab)))

Theorem: check-safe-variable-single-identifier-equiv-congruence-on-name

(defthm
     check-safe-variable-single-identifier-equiv-congruence-on-name
 (implies
   (identifier-equiv name name-equiv)
   (equal
        (check-safe-variable-single name init varset funtab)
        (check-safe-variable-single name-equiv init varset funtab)))
 :rule-classes :congruence)

Theorem: check-safe-variable-single-of-expression-option-fix-init

(defthm check-safe-variable-single-of-expression-option-fix-init
  (equal
       (check-safe-variable-single name (expression-option-fix init)
                                   varset funtab)
       (check-safe-variable-single name init varset funtab)))

Theorem: check-safe-variable-single-expression-option-equiv-congruence-on-init

(defthm
 check-safe-variable-single-expression-option-equiv-congruence-on-init
 (implies
   (expression-option-equiv init init-equiv)
   (equal
        (check-safe-variable-single name init varset funtab)
        (check-safe-variable-single name init-equiv varset funtab)))
 :rule-classes :congruence)

Theorem: check-safe-variable-single-of-identifier-set-fix-varset

(defthm check-safe-variable-single-of-identifier-set-fix-varset
 (equal
   (check-safe-variable-single name init (identifier-set-fix varset)
                               funtab)
   (check-safe-variable-single name init varset funtab)))

Theorem: check-safe-variable-single-identifier-set-equiv-congruence-on-varset

(defthm
 check-safe-variable-single-identifier-set-equiv-congruence-on-varset
 (implies
   (identifier-set-equiv varset varset-equiv)
   (equal
        (check-safe-variable-single name init varset funtab)
        (check-safe-variable-single name init varset-equiv funtab)))
 :rule-classes :congruence)

Theorem: check-safe-variable-single-of-funtable-fix-funtab

(defthm check-safe-variable-single-of-funtable-fix-funtab
  (equal (check-safe-variable-single
              name init varset (funtable-fix funtab))
         (check-safe-variable-single name init varset funtab)))

Theorem: check-safe-variable-single-funtable-equiv-congruence-on-funtab

(defthm
     check-safe-variable-single-funtable-equiv-congruence-on-funtab
 (implies
   (funtable-equiv funtab funtab-equiv)
   (equal
        (check-safe-variable-single name init varset funtab)
        (check-safe-variable-single name init varset funtab-equiv)))
 :rule-classes :congruence)