		Search-engine friendly clone of the ACL2 documentation.

Call-graphs

Call-graph-transunit

Build a call graph corresponding to a translation unit.

Signature
(call-graph-transunit filepath transunit call-graph) → call-graph$
Arguments: filepath — Guard (filepathp filepath).; transunit — Guard (transunitp transunit).; call-graph — Guard (call-graphp call-graph).
Returns: call-graph$ — Type (call-graphp call-graph$).

Definitions and Theorems

Function: call-graph-transunit

(defun call-graph-transunit (filepath transunit call-graph)
 (declare (xargs :guard (and (filepathp filepath)
                             (transunitp transunit)
                             (call-graphp call-graph))))
 (declare (xargs :guard (c$::transunit-annop transunit)))
 (let ((__function__ 'call-graph-transunit))
   (declare (ignorable __function__))
   (b*
    (((transunit transunit) transunit)
     (info (c$::transunit-info-fix (c$::transunit->info transunit)))
     (valid-table (c$::transunit-info->table info)))
    (call-graph-extdecl-list transunit.decls
                             filepath valid-table call-graph))))

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

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