		Search-engine friendly clone of the ACL2 documentation.

Call-graph

Call-graph-transunit

Build a call graph corresponding to a translation unit.

Signature
(call-graph-transunit transunit) → call-graph
Arguments: transunit — Guard (transunitp transunit).
Returns: call-graph — Type (ident-ident-option-set-mapp call-graph).

Definitions and Theorems

Function: call-graph-transunit

(defun call-graph-transunit (transunit)
  (declare (xargs :guard (transunitp transunit)))
  (let ((__function__ 'call-graph-transunit))
    (declare (ignorable __function__))
    (b* (((transunit transunit) transunit))
      (call-graph-extdecl-list transunit.decls nil))))

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

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