• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
          • Syntax-for-tools
          • Atc
          • Language
          • Representation
          • Transformation-tools
            • Simpadd0
            • Deftrans
            • Splitgso
            • Constant-propagation
            • Split-fn
            • Copy-fn
            • Specialize
            • Split-all-gso
            • Rename
            • Utilities
              • Free-vars
              • Call-graphs
                • Qualified-ident
                • Call-graph-transitive-closure
                • Qualified-ident-option
                • Call-graph-transitive-closure0
                • Call-graph-initdeclor-list
                • Call-graph-fundef
                • Call-graph-statassert
                • Call-graph-initdeclor
                • Call-graph-decl
                • Call-graph-const-expr
                • Call-graph-transunit
                • Call-graph-extdecl-list
                • Call-graph-extdecl
                • Call-graph-update
                • Qualify-ident
                • Exists-call-pathp
                • Call-graph-filepath-transunit-map
                • Uncertain-call-pathp
                • Recursivep
                • Direct-recursivep
                • Call-graph-transunit-ensemble
                • Call-graph
                • Qualified-ident-option-set
                • Direct-fun-refp
              • Fresh-ident-utility
              • Collect-idents
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Utilities

Call-graphs

Utilities to build a call graph from C translation units.

A call graph is a map from function names to the set of all functions which are called in the original function's body. For instance, consider the following C source file:

void bar(void);

void foo(int x) {
  foo(x);
  bar(x);
}

void bar(int x) {
  foo(x);
}

int baz(int z) {
  if (z) {
    return z;
  }
  return baz(z - 1);
}

int main() {
  int x = 5;
  return foo(x);
}

The call graph for this function would associate foo to foo and bar, bar to foo, baz to baz, and main to foo.

If a call graph edge connects a function to itself, this function is directly recursive. We may also construct the transitive closure of the call graph given some initial function call-graph-transitive-closure). This closure represents all functions which are reachable through some path of function calls. Notably, a mutually recursive function is in its own transitive closure. See direct-recursivep and recursivep.

Identifiers in the call graph are qualified to distinguish internal functions of the same name across different translation units. See qualified-ident.

Note that call graph construction currently only recognizes direct function calls. No sort of analysis is done to attempt to resolve calls of dereferenced function pointers. We may wish to add such analysis in the future. Although the problem is undecidable in general, many common cases may be straightforward in practice. Currently, a call of a function pointer is represented as nil in the call graph, so that we can distinguish between function call subgraphs which are known to be complete, and those which contain unresolved function calls. See also uncertain-call-pathp.

Subtopics

Qualified-ident
Fixtype for fully qualified identifiers
Call-graph-transitive-closure
Build a transitive closure for some identifier in the given call graph.
Qualified-ident-option
Option type; qualified-ident or nil.
Call-graph-transitive-closure0
Call-graph-initdeclor-list
Call-graph-fundef
Call-graph-statassert
Call-graph-initdeclor
Call-graph-decl
Call-graph-const-expr
Call-graph-transunit
Build a call graph corresponding to a translation unit.
Call-graph-extdecl-list
Call-graph-extdecl
Call-graph-update
Qualify-ident
Exists-call-pathp
Check for the existence of a call path from the destination to the target.
Call-graph-filepath-transunit-map
Uncertain-call-pathp
Recognizes functions which possess an unresolved function call path.
Recursivep
Recognizes directly or mutually recursive functions.
Direct-recursivep
Recognizes functions which calls themselves.
Call-graph-transunit-ensemble
Build a call graph corresponding to a translation unit ensemble.
Call-graph
An omap mapping qualified-identp to qualified-ident-option-setp.
Qualified-ident-option-set
A set of qualified-ident-optionp objects.
Direct-fun-refp