		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-term-guard-verified-exec-fns

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

Signature
(ensure-term-guard-verified-exec-fns term description error-erp error-val ctx state) → (mv erp val state)
Arguments: term — Term to check.
Guard (pseudo-termp term).; 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-term-guard-verified-exec-fns

(defun ensure-term-guard-verified-exec-fns
       (term description
             error-erp error-val ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termp term)
                             (msgp description))))
 (b*
  (((unless (guard-verified-exec-fnsp term (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 term (w state))))
       (if (= (len fns) 1)
           (msg "function ~x0" (car fns))
         (msg "functions ~&0" fns))))))
  (value nil)))

Subtopics

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