		Search-engine friendly clone of the ACL2 documentation.

Static-safety-checking

Check-safe-top-block

Check if the top block is safe.

Signature
(check-safe-top-block block) → _
Arguments: block — Guard (blockp block).
Returns: _ — Type (reserr-optionp _).

We check the safety of the block starting with no variables or functions in scope, because this is the block at the top level. Since the top block is not inside a function or loop, it is only allowed to terminate regularly. If the checking succeeds, we return nothing (i.e. nil). Otherwise, we return an error.

Definitions and Theorems

Function: check-safe-top-block

(defun check-safe-top-block (block)
  (declare (xargs :guard (blockp block)))
  (let ((__function__ 'check-safe-top-block))
    (declare (ignorable __function__))
    (b* (((okf modes)
          (check-safe-block block nil nil)))
      (if (equal modes (insert (mode-regular) nil))
          nil
        (reserrf (list :top-block-mode modes))))))

Theorem: reserr-optionp-of-check-safe-top-block

(defthm reserr-optionp-of-check-safe-top-block
  (b* ((_ (check-safe-top-block block)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: check-safe-top-block-of-block-fix-block

(defthm check-safe-top-block-of-block-fix-block
  (equal (check-safe-top-block (block-fix block))
         (check-safe-top-block block)))

Theorem: check-safe-top-block-block-equiv-congruence-on-block

(defthm check-safe-top-block-block-equiv-congruence-on-block
  (implies (block-equiv block block-equiv)
           (equal (check-safe-top-block block)
                  (check-safe-top-block block-equiv)))
  :rule-classes :congruence)