		Search-engine friendly clone of the ACL2 documentation.

Call-graphs

Uncertain-call-pathp

Recognizes functions which possess an unresolved function call path.

Signature
(uncertain-call-pathp ident call-graph) → *
Arguments: ident — Guard (qualified-identp ident).; call-graph — Guard (call-graphp 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 (qualified-identp ident)
                              (call-graphp call-graph))))
  (let ((__function__ 'uncertain-call-pathp))
    (declare (ignorable __function__))
    (exists-call-pathp ident nil call-graph)))