Atc-expression-generation
Generation of C expressions.
Subtopics
- Atc-gen-expr-struct-read-array
- Generate a C expression from an ACL2 term
that represents a structure array read.
- Atc-gen-expr-pure/bool
- Mutually recursive ACL2 functions to
generate pure C expressions from ACL2 terms.
- Atc-gen-expr-integer-read
- Generate a C expression from an ACL2 term
that represents an indirection of a pointer to integer.
- Atc-gen-expr-cond
- Generate a C expression from an ACL2 term
that represents a ternary conditional expression.
- Atc-gen-expr-binary
- Generate a C expression and theorem from an ACL2 term
that represents a binary expression.
- Atc-gen-expr-or
- Generate a C expressino from an ACL2 term
that represents a logical disjunction.
- Atc-gen-expr-array-read
- Generate a C expression from an ACL2 term
that represents an array read.
- Expr-gin
- Inputs for C pure expression generation.
- Exprs-gin
- Inputs for C pure expression list generation.
- Atc-gen-expr-and
- Generate a C expression from an ACL2 term
that represents a logical conjunction.
- Atc-gen-expr-struct-read-scalar
- Generate a C expression from an ACL2 term
that represents a structure scalar read.
- Exprs-gout
- Outputs for C pure expression list generation.
- Atc-gen-expr-unary
- Generate a C expression and theorem from an ACL2 term
that represents a unary expression.
- Atc-gen-expr-conv
- Generate a C expression from an ACL2 term
that represents an integer conversion.
- Expr-gout
- Outputs for C pure expression generation.
- Atc-gen-expr-bool-from-type
- Generate a C expression from an ACL2 term
that represents a conversion to ACL2 boolean.
- Atc-gen-expr-const
- Generate a C expression and theorem from an ACL2 term
that represents an integer constant expression.
- Atc-gen-expr-sint-from-bool
- Generate a C expression from an ACL2 term
that represents a conversion from ACL2 boolean.
- Atc-gen-expr-var
- Generate a C expression from an ACL2 variable.
- Atc-gen-expr-pure-list
- Generate a list of C expressions from a list of ACL2 terms
that must be pure expression terms returning C values.
- Irr-exprs-gout
- An irrelevant output for C pure expression list generation.
- Irr-expr-gout
- An irrelevant output for C pure expression generation.
