		Search-engine friendly clone of the ACL2 documentation.

Call-graphs

Call-graph-update

Signature
(call-graph-update fn-name called-fn-name? call-graph) → call-graph$
Arguments: fn-name — Guard (qualified-identp fn-name).; called-fn-name? — Guard (qualified-ident-optionp called-fn-name?).; call-graph — Guard (call-graphp call-graph).
Returns: call-graph$ — Type (call-graphp call-graph$).

Definitions and Theorems

Function: call-graph-update

(defun call-graph-update (fn-name called-fn-name? call-graph)
  (declare
       (xargs :guard (and (qualified-identp fn-name)
                          (qualified-ident-optionp called-fn-name?)
                          (call-graphp call-graph))))
  (let ((__function__ 'call-graph-update))
    (declare (ignorable __function__))
    (b* ((call-graph (call-graph-fix call-graph))
         (assoc (omap::assoc fn-name call-graph))
         (set (if assoc (cdr assoc) nil)))
      (omap::update
           (qualified-ident-fix fn-name)
           (insert (qualified-ident-option-fix called-fn-name?)
                   set)
           call-graph))))

Theorem: call-graphp-of-call-graph-update

(defthm call-graphp-of-call-graph-update
  (b* ((call-graph$
            (call-graph-update fn-name called-fn-name? call-graph)))
    (call-graphp call-graph$))
  :rule-classes :rewrite)