Guard-verified-exec-fnsp
Check if a term calls only guard-verified functions for execution.
- Signature
(guard-verified-exec-fnsp term wrld) → yes/no
- Arguments
- term — Guard (pseudo-termp term).
- wrld — Guard (plist-worldp wrld).
- Returns
- yes/no — A booleanp.
Check if all the functions that occur in the term, except possibly
the ones in the :logic subterms of mbes
and the ones called via ec-call,
are guard-verified.
The purpose of this function is to check whether a term
could be potentially guard-verified.
The name of this function is consistent with
the name of guard-verified-fnsp.
The all-fnnames-exec built-in system utility
returns all the function symbols except
the ones in the :logic subterms of mbes
and the ones called via ec-call
(see the ACL2 source code).
The collect-non-common-lisp-compliants built-in system utility
returns all the ones that are not guard-verified
(see the ACL2 source code).
Definitions and Theorems
Function: guard-verified-exec-fnsp
(defun guard-verified-exec-fnsp (term wrld)
(declare (xargs :guard (and (pseudo-termp term)
(plist-worldp wrld))))
(let ((__function__ 'guard-verified-exec-fnsp))
(declare (ignorable __function__))
(null (collect-non-common-lisp-compliants (all-fnnames-exec term)
wrld))))
