• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • 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
        • C
        • Soft
        • Bv
        • Imp-language
        • Ethereum
        • Event-macros
        • Java
        • Riscv
        • Bitcoin
        • Zcash
        • 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
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Axe
          • Lists-light
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Check-safe-statements/blocks/cases/fundefs

    Check-safe-statement-list

    Check if a list of statements is safe.

    Signature
    (check-safe-statement-list stmts varset funtab) → varsmodes
    Arguments
    stmts — Guard (statement-listp stmts).
    varset — Guard (identifier-setp varset).
    funtab — Guard (funtablep funtab).
    Returns
    varsmodes — Type (vars+modes-resultp varsmodes).

    We check the statements, one after the other, threading through the variable table.

    If the list of statements is empty, the termination mode is regular. Otherwise, we have a set of possible termination modes for the first statement, and a set of possible termination modes for the remaining sets. If the first set includes regular mode, we take the union of the two sets; otherwise, we just return the first set because execution of the list of statements ends there. Note that we still check the safety of the remaining statements, even when they are not reachable.