• 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
              • Escape
              • Swcase-list->value-list
              • Hex-digit-list->chars
              • Fundef-list->name-list
              • Literal
              • Path
              • Hex-string-rest-element
              • Plain-string
              • String-element
              • Hex-string-content-option
              • Hex-string-content
              • Identifier
              • Funcall-option
              • Expression-option
              • Statement-option
              • Literal-option
              • Identifier-option
              • Hex-string
              • Hex-quad
              • Hex-digit
              • Hex-pair
              • Data-value
              • Data-item
              • Statements-to-fundefs
              • String-element-list-result
              • Identifier-identifier-map-result
              • Swcase-result
              • String-element-result
              • Statement-result
              • Literal-result
              • Identifier-set-result
              • Identifier-result
              • Identifier-list-result
              • Fundef-result
              • Funcall-result
              • Expression-result
              • Escape-result
              • Path-result
              • Block-result
              • Objects
              • Statements/blocks/cases/fundefs
                • Statement
                  • Statement-case
                  • Statementp
                  • Statement-for
                  • Statement-equiv
                  • Statement-switch
                  • Statement-variable-single
                  • Statement-variable-multi
                  • Statement-if
                  • Statement-assign-single
                  • Statement-assign-multi
                  • Statement-kind
                  • Statement-fundef
                  • Statement-funcall
                  • Statement-block
                  • Statement-leave
                  • Statement-continue
                  • Statement-break
                  • Statement-fix
                  • Statement-count
                • Fundef
                • Block-option
                • Block
                • Swcase
                • Swcase-list
                • Statement-list
              • Identifier-list
              • Identifier-set
              • Identifier-identifier-map
              • Identifier-identifier-alist
              • Hex-string-rest-element-list
              • String-element-list
              • Path-list
              • Hex-digit-list
              • Literal-list
              • Fundef-list
              • Expressions/funcalls
              • Abstract-syntax-induction-schemas
            • Dynamic-semantics
            • Concrete-syntax
            • Static-soundness
            • Static-semantics
            • 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
  • Statements/blocks/cases/fundefs

Statement

Fixtype of statements.

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:block → statement-block
:variable-single → statement-variable-single
:variable-multi → statement-variable-multi
:assign-single → statement-assign-single
:assign-multi → statement-assign-multi
:funcall → statement-funcall
:if → statement-if
:for → statement-for
:switch → statement-switch
:leave → statement-leave
:break → statement-break
:continue → statement-continue
:fundef → statement-fundef

We use different constructors for declaration of single vs. multiple variables. We also use different constructors for assignments to single or mulitple paths. This way, we can restrict the use of function calls for multiple variables/targets, as opposed to general expressions for single variables/targets. The requirements that the lists of multiple variables or paths contain at least two elements are given in the static semantics. Also the requirement that switch statements have at least one case (literal or default) is given in the static semantics.

Subtopics

Statement-case
Case macro for the different kinds of statement structures.
Statementp
Recognizer for statement structures.
Statement-for
Statement-equiv
Basic equivalence relation for statement structures.
Statement-switch
Statement-variable-single
Statement-variable-multi
Statement-if
Statement-assign-single
Statement-assign-multi
Statement-kind
Get the kind (tag) of a statement structure.
Statement-fundef
Statement-funcall
Statement-block
Statement-leave
Statement-continue
Statement-break
Statement-fix
Fixing function for statement structures.
Statement-count
Measure for recurring over statement structures.