• 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-block

    Check if a block is safe.

    Signature
    (check-safe-block block varset funtab) → modes
    Arguments
    block — Guard (blockp block).
    varset — Guard (identifier-setp varset).
    funtab — Guard (funtablep funtab).
    Returns
    modes — Type (mode-set-resultp modes).

    If successful, return the set of possible termination modes of the block.

    As explained in add-funtypes, all the functions defined in a block are visible in the whole block, so we first collect them from the statements that form the block, updating the function table with them, and then we check the statements that form the block, discarding the final variable table.