		Search-engine friendly clone of the ACL2 documentation.

Call-graphs

Call-graph-fundef

Signature
(call-graph-fundef fundef filepath valid-table call-graph) → call-graph$
Arguments: fundef — Guard (fundefp fundef).; filepath — Guard (filepathp filepath).; valid-table — Guard (c$::valid-tablep valid-table).; call-graph — Guard (call-graphp call-graph).
Returns: call-graph$ — Type (call-graphp call-graph$).

Definitions and Theorems

Function: call-graph-fundef

(defun call-graph-fundef (fundef filepath valid-table call-graph)
 (declare (xargs :guard (and (fundefp fundef)
                             (filepathp filepath)
                             (c$::valid-tablep valid-table)
                             (call-graphp call-graph))))
 (let ((__function__ 'call-graph-fundef))
  (declare (ignorable __function__))
  (b* (((fundef fundef) fundef)
       ((declor fundef.declor) fundef.declor))
   (dirdeclor-case
     fundef.declor.direct :function-params
     (b*
       ((fn-name (c$::dirdeclor->ident fundef.declor.direct.declor))
        (qualified-fn-name
             (qualify-ident filepath valid-table fn-name)))
       (call-graph-stmt fundef.body qualified-fn-name
                        filepath valid-table call-graph))
     :function-names
     (b*
       ((fn-name (c$::dirdeclor->ident fundef.declor.direct.declor))
        (qualified-fn-name
             (qualify-ident filepath valid-table fn-name)))
       (call-graph-stmt fundef.body qualified-fn-name
                        filepath valid-table call-graph))
     :otherwise (call-graph-fix call-graph)))))

Theorem: call-graphp-of-call-graph-fundef

(defthm call-graphp-of-call-graph-fundef
  (b* ((call-graph$
            (call-graph-fundef fundef
                               filepath valid-table call-graph)))
    (call-graphp call-graph$))
  :rule-classes :rewrite)