		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-lambda-guard-verified-exec-fns

Cause an error if a lambda expression calls any non-guard-verified function for execution.

Signature
(ensure-lambda-guard-verified-exec-fns lambd description error-erp error-val ctx state) → (mv erp val state)
Arguments: lambd — Lambda expression to check.
Guard (pseudo-lambdap lambd).; description — Guard (msgp description).; error-erp — Flag to return in case of error.; error-val — Value to return in case of error.; ctx — Context for errors.
Returns: erp — nil or error-erp.; val — nil if erp is nil, otherwise error-val.

Definitions and Theorems

Function: ensure-lambda-guard-verified-exec-fns

(defun ensure-lambda-guard-verified-exec-fns
       (lambd description
              error-erp error-val ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-lambdap lambd)
                             (msgp description))))
 (b*
  (((unless (lambda-guard-verified-exec-fnsp lambd (w state)))
    (er-soft+
     ctx error-erp error-val
     "~@0 must call only guard-verified functions ~
     (except possibly in the :LOGIC subterms of MBEs and via EC-CALL), ~
     but it calls the non-guard-verified ~@1."
     description
     (let ((fns (all-non-gv-exec-ffn-symbs (lambda-body lambd)
                                           (w state))))
       (if (= (len fns) 1)
           (msg "function ~x0" (car fns))
         (msg "functions ~&0" fns))))))
  (value nil)))

Subtopics

Ensure-lambda-guard-verified-exec-fns$: Calls ensure-lambda-guard-verified-exec-fns with ctx and state as the last two arguments.