		Search-engine friendly clone of the ACL2 documentation.

Atc-event-and-code-generation

Term-checkers-atc

Checkers of ACL2 terms that represent C constructs, used by ATC.

These extend the ones in term-checkers-common.

Subtopics

Atc-check-cfun-call: Check if a term may represent a call to a C function, and in that case check the requirements on the call arguments.
Atc-check-struct-write-array: Check if a let binding may represent a structure write of an element of an array member.
Atc-check-struct-read-array: Check if a term may represent a structure read of an element of an array member.
Atc-check-struct-write-scalar: Check if a let binding may represent a structure write of a scalar member.
Atc-check-loop-call: Check if a term may represent a C loop.
Atc-check-struct-read-scalar: Check if a term may represent a structure read of a scalar member.
Atc-check-mv-let: Check if a term may be an mv-let statement term.
Atc-check-array-write: Check if a let binding may represent an array write.
Atc-check-let: Check if a term may be a let statement term.
Atc-check-array-read: Check if a term may represent an array read.
Atc-check-integer-write: Check if a term may represent a write of an integer by pointer.
Atc-check-declar/assign-n: Check if a term is a call of declar<n> or assign<n>.
Atc-check-condexpr: Check if a term may represent a C conditional expression.
Atc-check-boolean-from-type: Check if a term may represent a conversion from a C integer value to an ACL2 boolean.
Atc-check-integer-read: Check if a term may represent a read of an integer by pointer.
Atc-check-sint-from-boolean: Check if a term may represent a conversion from an ACL2 boolean to a C int value.