		Search-engine friendly clone of the ACL2 documentation.

Call-graph

Call-graph-fundef

Signature
(call-graph-fundef fundef acc) → call-graph
Arguments: fundef — Guard (fundefp fundef).; acc — Guard (ident-ident-option-set-mapp acc).
Returns: call-graph — Type (ident-ident-option-set-mapp call-graph).

Definitions and Theorems

Function: call-graph-fundef

(defun call-graph-fundef (fundef acc)
 (declare (xargs :guard (and (fundefp fundef)
                             (ident-ident-option-set-mapp acc))))
 (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 (dirdeclor-get-ident fundef.declor.direct.decl)))
       (call-graph-stmt fundef.body fn-name acc))
     :function-names
     (b* ((fn-name (dirdeclor-get-ident fundef.declor.direct.decl)))
       (call-graph-stmt fundef.body fn-name acc))
     :otherwise (ident-ident-option-set-map-fix acc)))))

Theorem: ident-ident-option-set-mapp-of-call-graph-fundef

(defthm ident-ident-option-set-mapp-of-call-graph-fundef
  (b* ((call-graph (call-graph-fundef fundef acc)))
    (ident-ident-option-set-mapp call-graph))
  :rule-classes :rewrite)