		Search-engine friendly clone of the ACL2 documentation.

Language

Static-semantics

A static semantics of C.

This static semantics consists of ACL2 functions that check whether the abstract syntactic entities satisfy the needed constraints. If the constraints are satisfied, additional information (e.g. types) may be returned, used to check constraints on enclosing abstract syntactic entities.

Subtopics

Check-stmt: Check a statement.
Check-cond: Check a ternary conditional expression [C:6.5.15].
Check-binary-pure: Check the application of a pure binary operator to two expressions.
Var-table-add-var: Add a variable to (the innermost scope of) a variable table.
Check-unary: Check the application of a unary operator to an expression.
Check-obj-declon: Check an object declaration.
Fun-table-add-fun: Add static information about a function to a function table.
Fun-sinfo: Fixtype of static information about functions.
Check-fundef: Check a function definition.
Check-expr-asg: Check an expression that must be an assignment expression.
Check-expr-call: Check an expression that is a function call.
Check-arrsub: Check an array subscripting expression [C:6.5.2.1].
Uaconvert-types: Apply the usual arithmetic conversions to two arithmetic types [C:6.3.1.8].
Apconvert-type-list: Lift apconvert-type to lists.
Check-initer: Check an initializer.
Adjust-type-list: Lift adjust-type to lists.
Types+vartab: Fixtype of pairs consisting of a non-empty set of types and a variable table.
Promote-type: Apply the integer promotions to an arithmetic type [C:6.3.1.1/2].
Check-tag-declon: Check a tag declaration.
Check-expr-call-or-asg: Check an expression that must be a function call or an assignment.
Check-param-declon: Check a parameter declaration.
Check-ext-declon: Check an external declaration.
Check-member: Check a structure member expression [C:6.5.2.3].
Check-expr-pure: Check a pure expression.
Check-obj-adeclor: Check an abstract object declarator.
Check-memberp: Check a structure pointer member expression [C:6.5.2.3].
Check-expr-call-or-pure: Check an expression that must be a function call or a pure expression.
Check-cast: Check a cast expression [C:6.5.4].
Init-type-matchp: Check if an initializer type matches a type.
Check-struct-declon-list: Check a list of structure declarations.
Check-fun-declor: Check a function declarator.
Expr-type: Fixtype of expression types.
Check-ext-declon-list: Check a list of external declarations.
Check-transunit: Check a translation unit.
Check-fun-declon: Check a function declaration.
Var-defstatus: Fixtype of definition statuses of variables.
Struct-member-lookup: Look up a member in a structure type in the tag environment.
Preprocess: Preprocess a file set [C:5.1.1.2/4].
Wellformed: Fixtype of the well-formedness indicator.
Check-tyspecseq: Check a type specifier sequence.
Check-param-declon-list: Check a list of parameter declarations.
Check-iconst: Check an integer constant.
Check-expr-pure-list: Check a list of pure expressions.
Var-sinfo-option: Fixtype of optional static information about variables.
Fun-sinfo-option: Fixtype of optional static information about functions.
Var-scope-all-definedp: CHeck if all the variables in a scope are defined.
Funtab+vartab+tagenv: Fixtype of triples consisting of a function table, a variable table, and a tag environment.
Var-sinfo: Fixtype of static information about variables.
Var-table-lookup: Look up a variable in a variable table.
Apconvert-type: Convert array type to pointer type.
Var-table: Fixtype of variable tables, i.e. symbol tables for variables.
Check-tyname: Check a type name.
Types+vartab-result: Fixtype of errors and pairs consisting of a non-empty set of types and a variable table.
Funtab+vartab+tagenv-result: Fixtype of errors and triples consisting of a function table, a variable table, and a tag environment.
Fun-table-lookup: Look up a function in a function table.
Wellformed-result: Fixtype of errors and the wellformed indicator.
Var-table-add-block: Add a block scope to a variable table.
Var-table-scope: Fixtype of scopes of variable tables.
Var-table-result: Fixtype of errors and variable tables.
Fun-table-result: Fixtype of errors and function tables.
Expr-type-result: Fixtype of errors and expression types.
Adjust-type: Adjust a parameter type.
Check-fileset: Check a file set.
Var-table-all-definedp: CHeck if all the variables in a file scope are defined.
Check-const: Check a constant.
Fun-table-all-definedp: Check if all the functions in a table are defined.
Check-ident: Check an identifier.
Fun-table: Fixtype of function tables, i.e. symbol tables for functions.
Var-table-init: Create an initial variable table.
Fun-table-init: Create an initial function table.