		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Abstract-syntax-operations

Operations on the C abstract syntax.

Subtopics

Tyspec+declor-to-ident+params+tyname: Turn a type specifier sequence and a function declarator into an identifier, a list of parameter declarations, and a type name.
Fundef-list-to-fun-declon-list: Lift fundef-to-fun-declon to lists.
Fundef-list->name-list: Lift fundef->name to lists.
Ident+tyname-to-tyspec+declor: Turn an identifier and a type name into a type specifier sequence and an object declarator.
Tyspec+declor-to-ident+tyname: Turn a type specifier sequence and an object declarator into an identifier and a type name.
Obj-declon-to-ident+scspec+tyname+init: Decompose an object declaration into an identifier, a storage class specifier sequence, a type name, and an optional initializer.
Ident+adeclor-to-obj-declor: Compose an identifier and an abstract object declarator into an object declarator.
Ident+adeclor-to-fun-declor: Compose an identifier and an abstract function declarator into a function declarator.
Fun-adeclor-to-params+declor: Decompose an abstract function declarator into a list of parameter declarations and an abstract object declarator.
Param-declon-list-to-ident+tyname-lists: Lift param-declon-to-ident+tyname to lists.
Obj-declor-to-ident+adeclor: Decompose an object declarator into an identifier and an abstract object declarator.
Fun-declor-to-ident+adeclor: Decompose a function declarator into an identifier and an abstract function declarator.
Expr-constp: Check if an expression is constant.
Fundef-to-fun-declon: Function declaration of a function definition.
Param-declon-to-ident+tyname: Decompose a parameter declaration into an identifier and a type name.
Ext-declon-list->fundef-list: Extract from a list of external declarations the list of function definitions, in the same order.
Struct-declon-to-ident+tyname: Decompose a structure declaration into an identifier and a type name.
Unop-nonpointerp: Check if a unary operator does not involve pointers.
Binop-strictp: Check if a binary operator is strict.
Expr-list-constp: Lift expr-constp to lists.
Binop-purep: Check if a binary operator is pure.
Fundef->name: Name of a function in a definition.