• 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
          • Syntax-for-tools
          • Atc
            • Atc-implementation
              • Atc-abstract-syntax
              • Atc-pretty-printer
              • Atc-event-and-code-generation
                • Atc-symbolic-computation-states
                • Atc-symbolic-execution-rules
                • Atc-gen-ext-declon-lists
                • Atc-function-and-loop-generation
                • Atc-statement-generation
                • Atc-gen-fileset
                • Atc-gen-everything
                • Atc-gen-obj-declon
                • Atc-gen-fileset-event
                • Atc-tag-tables
                • Atc-expression-generation
                  • Atc-gen-expr-struct-read-array
                  • Atc-gen-expr-pure/bool
                  • Atc-gen-expr-integer-read
                  • Atc-gen-expr-cond
                  • Atc-gen-expr-binary
                  • Atc-gen-expr-or
                  • Atc-gen-expr-array-read
                  • Expr-gin
                  • Exprs-gin
                  • Atc-gen-expr-and
                  • Atc-gen-expr-struct-read-scalar
                  • Exprs-gout
                    • Exprs-gout-fix
                    • Make-exprs-gout
                    • Exprs-gout-equiv
                    • Exprs-goutp
                    • Exprs-gout->names-to-avoid
                    • Exprs-gout->thm-names
                    • Exprs-gout->events
                    • Change-exprs-gout
                    • Exprs-gout->types
                    • Exprs-gout->thm-index
                    • Exprs-gout->terms
                    • Exprs-gout->exprs
                  • Atc-gen-expr-unary
                  • Atc-gen-expr-conv
                  • Expr-gout
                  • Atc-gen-expr-bool-from-type
                  • Atc-gen-expr-const
                  • Atc-gen-expr-sint-from-bool
                  • Atc-gen-expr-var
                  • Atc-gen-expr-pure-list
                  • Irr-exprs-gout
                  • Irr-expr-gout
                • Atc-generation-contexts
                • Atc-gen-wf-thm
                • Term-checkers-atc
                • Atc-variable-tables
                • Term-checkers-common
                • Atc-gen-init-fun-env-thm
                • Atc-gen-appconds
                • Read-write-variables
                • Atc-gen-thm-assert-events
                • Test*
                • Atc-gen-prog-const
                • Atc-gen-expr-bool
                • Atc-theorem-generation
                • Atc-tag-generation
                • Atc-gen-expr-pure
                • Atc-function-tables
                • Atc-object-tables
              • Fty-pseudo-term-utilities
              • Atc-term-recognizers
              • Atc-input-processing
              • Atc-shallow-embedding
              • Atc-process-inputs-and-gen-everything
              • Atc-table
              • Atc-fn
              • Atc-pretty-printing-options
              • Atc-types
              • Atc-macro-definition
            • Atc-tutorial
          • Language
          • Representation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • 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
  • Atc-expression-generation

Exprs-gout

Outputs for C pure expression list generation.

This is a product type introduced by fty::defprod.

Fields
exprs — expr-list
Expressions generated from the term.
types — type-list
The types returned by the expressions, in order. None of these is void.
terms — pseudo-term-list
The terms from which the expressions are generated, in order. The terms are transformed by replacing if with if*.
events — pseudo-event-form-list
All the events generated for the expressions.
thm-names — symbol-list
The name of the theorems about exec-expr-pure applied to the expressions. These theorems are some of the events in events. These are all nil if no theorems were generated, which happens exactly when the proofs flag in expr-gin is nil.
thm-index — posp
Described in atc-implementation.
names-to-avoid — symbol-list
Described in atc-implementation.

Subtopics

Exprs-gout-fix
Fixing function for exprs-gout structures.
Make-exprs-gout
Basic constructor macro for exprs-gout structures.
Exprs-gout-equiv
Basic equivalence relation for exprs-gout structures.
Exprs-goutp
Recognizer for exprs-gout structures.
Exprs-gout->names-to-avoid
Get the names-to-avoid field from a exprs-gout.
Exprs-gout->thm-names
Get the thm-names field from a exprs-gout.
Exprs-gout->events
Get the events field from a exprs-gout.
Change-exprs-gout
Modifying constructor for exprs-gout structures.
Exprs-gout->types
Get the types field from a exprs-gout.
Exprs-gout->thm-index
Get the thm-index field from a exprs-gout.
Exprs-gout->terms
Get the terms field from a exprs-gout.
Exprs-gout->exprs
Get the exprs field from a exprs-gout.