• 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
        • Soft
        • Bv
        • Imp-language
        • C
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
          • Transformations
          • Language
            • Abstract-syntax
            • Dynamic-semantics
              • Exec
                • Exec-statement
                • Exec-function
                • Exec-for-iterations
                • Exec-block
                • Exec-switch-rest
                • Exec-expression-list
                • Exec-funcall
                • Exec-statement-list
                • Exec-expression
                • Find-fun
                • Init-local
                • Mode
                • Write-vars-values
                • Add-vars-values
                • Add-funs
                • Eoutcome
                • Soutcome
                • Ensure-funscope-disjoint
                • Write-var-value
                • Restrict-vars
                • Add-var-value
                • Funinfo
                • Exec-top-block
                • Values
                • Cstate
                • Funinfo+funenv
                • Read-vars-values
                • Read-var-value
                • Funenv
                • Funscope-for-fundefs
                • Exec-path
                • Path-to-var
                • Funinfo+funenv-result
                • Exec-literal
                • Soutcome-result
                • Mode-set-result
                • Funscope-result
                • Funinfo-result
                • Funenv-result
                • Eoutcome-result
                • Cstate-result
                • Paths-to-vars
                • Funinfo-for-fundef
                • Literal-evaluation
                • Lstate
                • Funscope
                • Mode-set
              • Concrete-syntax
              • Static-soundness
              • Static-semantics
              • Errors
            • Yul-json
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Number-theory
          • Cryptography
          • Lists-light
          • Builtins
          • Axe
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Exec

    Exec-expression

    Execute an expression.

    Signature
    (exec-expression expr cstate funenv limit) → outcome
    Arguments
    expr — Guard (expressionp expr).
    cstate — Guard (cstatep cstate).
    funenv — Guard (funenvp funenv).
    limit — Guard (natp limit).
    Returns
    outcome — Type (eoutcome-resultp outcome).