		Search-engine friendly clone of the ACL2 documentation.

Call-graph

Uncertain-call-pathp

Recognizes functions which possess an unresolved function call path.

Signature
(uncertain-call-pathp ident call-graph) → *
Arguments: ident — Guard (identp ident).; call-graph — Guard (ident-ident-option-set-mapp call-graph).

This function checks whether nil is in ident's transitive closure. See call-graph-transitive-closure and (see call-graph).

Definitions and Theorems

Function: uncertain-call-pathp

(defun uncertain-call-pathp (ident call-graph)
 (declare
      (xargs :guard (and (identp ident)
                         (ident-ident-option-set-mapp call-graph))))
 (let ((__function__ 'uncertain-call-pathp))
   (declare (ignorable __function__))
   (exists-call-pathp ident nil call-graph)))