		Search-engine friendly clone of the ACL2 documentation.

Atc-event-and-code-generation

Atc-statement-generation

Generation of C statements.

Subtopics

Stmt-gin: Inputs for C statement generation.
Atc-gen-term-type-formula: Generate a type formula for a term.
Atc-gen-stmt: Generate a C statement from an ACL2 term.
Stmt-gout: Outputs for C statement generation.
Atc-gen-expr: Generate a C expression from an ACL2 term that must be an expression term.
Atc-gen-block-item-var-asg: Generate a C block item statement that consists of an assignment to a variable.
Atc-gen-return-stmt: Generate a C return statement from an ACL2 term.
Atc-gen-mbt-block-items: Generate a list of block items from an ACL2 conditional with an mbt test.
Atc-gen-if/ifelse-stmt: Generate a C if or if-else statement from an ACL2 term.
Atc-gen-cfun-call-stmt: Generate a C block item statement that consists of a call of a void function.
Atc-gen-block-item-struct-scalar-asg: Generate a C block item statement that consists of an assignment to a scalar member of a structure.
Atc-gen-block-item-struct-array-asg: Generate a C block item statement that consists of an assignment to an element of an array member of a structure.
Atc-gen-block-item-list-append: Generate a list of block items by appending two lists of block items.
Atc-gen-block-item-integer-asg: Generate a C block item statement that consists of an assignment to a pointed integer.
Atc-gen-block-item-declon: Generate a C block item that consists of an object declaration.
Atc-gen-block-item-array-asg: Generate a C block item statement that consists of an assignment to an array element.
Atc-gen-loop-stmt: Generate a C loop statement from an ACL2 term.
Atc-gen-block-item-list-cons: Generate a list of block items by consing a block item to a list of block items.
Atc-uterm-to-components: Split a term into component terms.
Atc-gen-block-item-stmt: Generate a C block item that consists of a given statement.
Lstmt-gin: Inputs for C loop statement generation.
Atc-gen-block-item-list-one: Generate a list of C block items that consists of a given item.
Atc-gen-block-item-var-decl: Generate a C block item statement that consists of a variable declaration.
Atc-gen-block-item-asg: Generate a C block item that consists of a given assignment.
Atc-gen-call-result-and-endstate: Generate a term representing the result value and a term representing the ending computation state of the execution of a C function call.
Lstmt-gout: Outputs for C loop statement generation.
Atc-ensure-formals-not-lost: Ensure that no affected formals are lost.
Atc-gen-block-item-list-none: Generate an empty list of block items.
Atc-var-assignablep: Check if a variable is assignable, based on whether it is in the innermost scope and based on the variables being currently affected.
Atc-gen-uterm-result-and-type-formula: Generates a result term and a type formula for a term.
Atc-remove-extobj-args: Remove from a list of argument terms the ones that are external objects.
Atc-affecting-term-for-let-p: Check if a term term has the basic structure required for representing code affecting variables in (let ((var term)) body) or (mv-let (var1 ... varn) term body).
Atc-vars-assignablep: Lift atc-var-assignablep to lists.
Atc-make-lets-of-uterms: Create a list of lets or let*s with the same bindings and with bodies from a list of terms, in the same order.
Atc-symbolp-list: Check if each element of a list is a symbol or not, returning a list of booleans, one per element.
Atc-make-mv-nth-terms: Create a list of mv-nths applied to a term for a list of indices.
Atc-make-mv-lets-of-uterms: Create a list of mv-lets with the same bindings and with bodies from a list of terms, in the same order.
Atc-update-var-term-alist: Update an alist from symbols to terms.
Irr-stmt-gout: An irrelevant output for C statement generation.
Irr-lstmt-gout: An irrelevant output for C loop statement generation.