		Search-engine friendly clone of the ACL2 documentation.

Call-graphs

Call-graph-decl

Signature
(call-graph-decl decl fn-name filepath valid-table call-graph) → call-graph$
Arguments: decl — Guard (declp decl).; fn-name — Guard (qualified-identp fn-name).; filepath — Guard (filepathp filepath).; valid-table — Guard (c$::valid-tablep valid-table).; call-graph — Guard (call-graphp call-graph).
Returns: call-graph$ — Type (call-graphp call-graph$).

Definitions and Theorems

Function: call-graph-decl

(defun call-graph-decl
       (decl fn-name filepath valid-table call-graph)
  (declare (xargs :guard (and (declp decl)
                              (qualified-identp fn-name)
                              (filepathp filepath)
                              (c$::valid-tablep valid-table)
                              (call-graphp call-graph))))
  (let ((__function__ 'call-graph-decl))
    (declare (ignorable __function__))
    (decl-case
         decl
         :decl (call-graph-initdeclor-list
                    decl.init
                    fn-name filepath valid-table call-graph)
         :statassert
         (call-graph-statassert decl.unwrap fn-name
                                filepath valid-table call-graph))))

Theorem: call-graphp-of-call-graph-decl

(defthm call-graphp-of-call-graph-decl
  (b*
   ((call-graph$ (call-graph-decl decl fn-name
                                  filepath valid-table call-graph)))
   (call-graphp call-graph$))
  :rule-classes :rewrite)