• 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
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
          • Transformations
          • Language
            • Abstract-syntax
            • Dynamic-semantics
            • Concrete-syntax
            • Static-soundness
            • Static-semantics
              • Static-safety-checking
                • Check-safe-statements/blocks/cases/fundefs
                • Check-safe-expressions
                  • Check-safe-expression-list
                  • Check-safe-expression
                  • Check-safe-funcall
                  • Check-safe-fundef-list
                  • Check-safe-variable-multi
                  • Check-safe-variable-single
                  • Check-safe-assign-multi
                  • Check-safe-assign-single
                  • Check-safe-path
                  • Check-safe-extends-varset
                  • Vars+modes
                  • Add-vars
                  • Add-var
                  • Add-funtypes
                  • Check-safe-literal
                  • Funtype
                  • Get-funtype
                  • Check-var
                  • Check-safe-top-block
                  • Check-safe-path-list
                  • Vars+modes-result
                  • Funtype-result
                  • Funtable-result
                  • Funtable-for-fundefs
                  • Funtype-for-fundef
                  • Funtable
                • Static-shadowing-checking
                • Mode-set-result
                • Literal-evaluation
                • Static-identifier-checking
                • Static-safety-checking-evm
                • Mode-set
                • Modes
              • Errors
            • Yul-json
          • 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
    • Check-safe-expressions

    Check-safe-funcall

    Check if a function call is safe.

    Signature
    (check-safe-funcall call varset funtab) → results?
    Arguments
    call — Guard (funcallp call).
    varset — Guard (identifier-setp varset).
    funtab — Guard (funtablep funtab).
    Returns
    results? — Type (nat-resultp results?).

    We look up the function in the function table, which is passed as parameter. We ensure that the number of inputs matches, and we return the number of outputs. Each argument expression must return a single result.