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

    Check if an expression is safe.

    Signature
    (check-safe-expression expr varset funtab) → results?
    Arguments
    expr — Guard (expressionp expr).
    varset — Guard (identifier-setp varset).
    funtab — Guard (funtablep funtab).
    Returns
    results? — Type (nat-resultp results?).

    If successful, return the number of values that the expression yields. Otherwise, return an error.

    A path always yields one result.

    A literal's safety is independent from the variables in scope. A literal always returns one result.