• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Riscv
      • Taspi
      • Bitcoin
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Aleo
        • Aleobft
        • Aleovm
        • Leo
          • Grammar
          • Early-version
            • Json2ast
            • Testing
            • Definition
              • Flattening
              • Abstract-syntax
              • Dynamic-semantics
              • Compilation
              • Static-semantics
                • Type-checking
                • Static-environments
                • Curve-parameterization
                • Function-recursion
                  • Statements-callees
                  • Expressions-callees
                  • File-function-recursion-okp
                  • Topdecl-list-call-graph
                  • Fundecl-call-graph
                  • Topdecl-call-graph
                  • Expression-callees
                    • Constdecl-callees
                    • Console-callees
                    • Vardecl-callees
                    • Struct-init-list-callees
                    • Struct-init-callees
                    • Statement-list-callees
                    • Expression-list-callees
                    • Branch-list-callees
                    • Statement-callees
                    • Branch-callees
                  • Struct-recursion
                  • Input-checking
                  • Program-checking
                  • Type-maps-for-struct-components
                  • Program-and-input-checking
                  • Output-checking
                • Concrete-syntax
        • Bigmems
        • Builtins
        • Execloader
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Community
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Function-recursion
    • Expressions-callees

    Expression-callees

    Functions called by an expression.

    Signature
    (expression-callees expr) → callees
    Arguments
    expr — Guard (expressionp expr).
    Returns
    callees — Type (identifier-setp callees).

    If a non-static struct member function call is not resolved (i.e. it does not have the struct type name), we return nil. Thus, this is correct only if that struct type name is present, i.e. if the function recursion check is performed after type inference. We will enforce this by defining a predicate requiring the presence of the struct type name and using that as guard of this ACL2 function.