All-non-gv-exec-ffn-symbs
Non-guard-verified functions called by a term for execution.
- Signature
(all-non-gv-exec-ffn-symbs term wrld) → final-ans
- Arguments
- term — Guard (pseudo-termp term).
- wrld — Guard (plist-worldp wrld).
- Returns
- final-ans — A symbol-listp.
These are all the non-guard-verified functions that occur in the term,
except those that occur in the :logic subterms of mbes
and those called via ec-call.
This is because, in order for a function to be guard-verified,
the functions that occurs in such subterms do not have to be guard-verified.
If this function returns nil,
the term could be potentially guard-verified.
The name of this function is consistent with
the name of all-ffn-symbs in the ACL2 source code.
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: all-non-gv-exec-ffn-symbs
(defun
all-non-gv-exec-ffn-symbs (term wrld)
(declare (xargs :guard (and (pseudo-termp term)
(plist-worldp wrld))))
(let ((__function__ 'all-non-gv-exec-ffn-symbs))
(declare (ignorable __function__))
(collect-non-common-lisp-compliants (all-fnnames-exec term)
wrld)))
