		Search-engine friendly clone of the ACL2 documentation.

Call-graphs

Call-graph-transunit-ensemble

Build a call graph corresponding to a translation unit ensemble.

Signature
(call-graph-transunit-ensemble ensemble) → call-graph$
Arguments: ensemble — Guard (transunit-ensemblep ensemble).
Returns: call-graph$ — Type (call-graphp call-graph$).

Definitions and Theorems

Function: call-graph-transunit-ensemble

(defun call-graph-transunit-ensemble (ensemble)
  (declare (xargs :guard (transunit-ensemblep ensemble)))
  (declare (xargs :guard (transunit-ensemble-annop ensemble)))
  (let ((__function__ 'call-graph-transunit-ensemble))
    (declare (ignorable __function__))
    (call-graph-filepath-transunit-map
         (transunit-ensemble->units ensemble)
         nil)))

Theorem: call-graphp-of-call-graph-transunit-ensemble

(defthm call-graphp-of-call-graph-transunit-ensemble
  (b* ((call-graph$ (call-graph-transunit-ensemble ensemble)))
    (call-graphp call-graph$))
  :rule-classes :rewrite)