• 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
          • 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
                  • Pexprs-gin
                  • Atc-gen-expr-and
                  • Atc-gen-expr-struct-read-scalar
                  • Pexprs-gout
                    • Pexprs-gout-fix
                    • Make-pexprs-gout
                    • Pexprs-gout-equiv
                    • Pexprs-goutp
                    • Pexprs-gout->names-to-avoid
                    • Change-pexprs-gout
                    • Pexprs-gout->thm-names
                    • Pexprs-gout->thm-index
                    • Pexprs-gout->terms
                    • Pexprs-gout->events
                    • Pexprs-gout->types
                    • Pexprs-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-pexprs-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
          • Pack
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • 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
  • Atc-expression-generation

Pexprs-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

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