		Search-engine friendly clone of the ACL2 documentation.

Call-graph

Call-graph-update

Signature
(call-graph-update fn-name called-fn-name call-graph) → new-call-graph
Arguments: fn-name — Guard (identp fn-name).; called-fn-name — Guard (ident-optionp called-fn-name).; call-graph — Guard (ident-ident-option-set-mapp call-graph).
Returns: new-call-graph — Type (ident-ident-option-set-mapp new-call-graph).

Definitions and Theorems

Function: call-graph-update

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

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

(defthm ident-ident-option-set-mapp-of-call-graph-update
  (b* ((new-call-graph
            (call-graph-update fn-name called-fn-name call-graph)))
    (ident-ident-option-set-mapp new-call-graph))
  :rule-classes :rewrite)