		Search-engine friendly clone of the ACL2 documentation.

Static-safety-checking

Check-safe-assign-single

Check if a single assignment is safe.

Signature
(check-safe-assign-single target value varset funtab) → _
Arguments: target — Guard (pathp target).; value — Guard (expressionp value).; varset — Guard (identifier-setp varset).; funtab — Guard (funtablep funtab).
Returns: _ — Type (reserr-optionp _).

Similarly to check-safe-expression, for now we require the path to be a singleton; see discussion there about non-singleton paths.

We check the expression, and and ensure that it returns one result.

Definitions and Theorems

Function: check-safe-assign-single

(defun check-safe-assign-single (target value varset funtab)
  (declare (xargs :guard (and (pathp target)
                              (expressionp value)
                              (identifier-setp varset)
                              (funtablep funtab))))
  (let ((__function__ 'check-safe-assign-single))
    (declare (ignorable __function__))
    (b* (((okf &)
          (check-safe-path target varset))
         ((okf results)
          (check-safe-expression value varset funtab))
         ((unless (= results 1))
          (reserrf (list :assign-single-var-mismatch
                         (path-fix target)
                         results))))
      nil)))

Theorem: reserr-optionp-of-check-safe-assign-single

(defthm reserr-optionp-of-check-safe-assign-single
  (b* ((_ (check-safe-assign-single target value varset funtab)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: check-safe-assign-single-of-path-fix-target

(defthm check-safe-assign-single-of-path-fix-target
  (equal (check-safe-assign-single (path-fix target)
                                   value varset funtab)
         (check-safe-assign-single target value varset funtab)))

Theorem: check-safe-assign-single-path-equiv-congruence-on-target

(defthm check-safe-assign-single-path-equiv-congruence-on-target
 (implies
  (path-equiv target target-equiv)
  (equal
       (check-safe-assign-single target value varset funtab)
       (check-safe-assign-single target-equiv value varset funtab)))
 :rule-classes :congruence)

Theorem: check-safe-assign-single-of-expression-fix-value

(defthm check-safe-assign-single-of-expression-fix-value
  (equal (check-safe-assign-single target (expression-fix value)
                                   varset funtab)
         (check-safe-assign-single target value varset funtab)))

Theorem: check-safe-assign-single-expression-equiv-congruence-on-value

(defthm
      check-safe-assign-single-expression-equiv-congruence-on-value
 (implies
  (expression-equiv value value-equiv)
  (equal
       (check-safe-assign-single target value varset funtab)
       (check-safe-assign-single target value-equiv varset funtab)))
 :rule-classes :congruence)

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

(defthm check-safe-assign-single-of-identifier-set-fix-varset
 (equal
  (check-safe-assign-single target value (identifier-set-fix varset)
                            funtab)
  (check-safe-assign-single target value varset funtab)))

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

(defthm
 check-safe-assign-single-identifier-set-equiv-congruence-on-varset
 (implies
  (identifier-set-equiv varset varset-equiv)
  (equal
       (check-safe-assign-single target value varset funtab)
       (check-safe-assign-single target value varset-equiv funtab)))
 :rule-classes :congruence)

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

(defthm check-safe-assign-single-of-funtable-fix-funtab
  (equal
       (check-safe-assign-single target
                                 value varset (funtable-fix funtab))
       (check-safe-assign-single target value varset funtab)))

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

(defthm check-safe-assign-single-funtable-equiv-congruence-on-funtab
 (implies
  (funtable-equiv funtab funtab-equiv)
  (equal
       (check-safe-assign-single target value varset funtab)
       (check-safe-assign-single target value varset funtab-equiv)))
 :rule-classes :congruence)