• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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-statement
                  • Check-safe-fundef
                    • Check-safe-statement-list
                    • Check-safe-block
                    • Check-safe-swcase-list
                    • Check-safe-block-option
                    • Check-safe-swcase
                  • Check-safe-expressions
                  • 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-statements/blocks/cases/fundefs

    Check-safe-fundef

    Check if a function definition is safe.

    Signature
    (check-safe-fundef fundef funtab) → _
    Arguments
    fundef — Guard (fundefp fundef).
    funtab — Guard (funtablep funtab).
    Returns
    _ — Type (reserr-optionp _).

    This ACL2 function takes as input less contextual information than its mutually recursive companions. The reason is that such contextual information is always set when a funtion definition is checked. In particular, there is no variable table to pass.

    This ACL2 function does not need to return anything. Any variable table internal to the function's body does not surface outside the function's body. Also recall that the function definition itself is added to the function table prior to checking it; see add-funtypes.

    To check the function definition, we construct an initial variable table from the inputs and outputs of the function. Note that the construction will detect and reject any duplicates. Then we check the function's body, ensuring that it does not end with break or continue, (i.e. only with leave or regularly).