		Search-engine friendly clone of the ACL2 documentation.

Function-recursion

Fundecl-call-graph

Call graph induced by a function declaration.

Signature
(fundecl-call-graph decl) → graph
Arguments: decl — Guard (fundeclp decl).
Returns: graph — Type (alistp graph).

We return a dependency graph expressing that the declared function depends on (i.e. calls) the functions directly called in its body. The format is that of an alist for the dependency graph library.

Definitions and Theorems

Function: fundecl-call-graph

(defun fundecl-call-graph (decl)
  (declare (xargs :guard (fundeclp decl)))
  (let ((__function__ 'fundecl-call-graph))
    (declare (ignorable __function__))
    (b* (((fundecl decl) decl)
         (caller decl.name)
         (callees (statement-list-callees decl.body)))
      (list (cons caller callees)))))

Theorem: alistp-of-fundecl-call-graph

(defthm alistp-of-fundecl-call-graph
  (b* ((graph (fundecl-call-graph decl)))
    (alistp graph))
  :rule-classes :rewrite)

Theorem: fundecl-call-graph-of-fundecl-fix-decl

(defthm fundecl-call-graph-of-fundecl-fix-decl
  (equal (fundecl-call-graph (fundecl-fix decl))
         (fundecl-call-graph decl)))

Theorem: fundecl-call-graph-fundecl-equiv-congruence-on-decl

(defthm fundecl-call-graph-fundecl-equiv-congruence-on-decl
  (implies (fundecl-equiv decl decl-equiv)
           (equal (fundecl-call-graph decl)
                  (fundecl-call-graph decl-equiv)))
  :rule-classes :congruence)