Abstract-syntax
A preliminary abstract syntax of C.
This abstract syntax is preliminary in the sense that
it is neither general nor complete.
It is not general because it assumes the use of ASCII characters.
which is not necessarily the case according to [C].
It is not complete because it does not cover all the C constructs.
Nonetheless, it covers a useful and interesting subset of C,
with the ASCII assumption being largely supported
(as part of perhaps a larger character set like Unicode).
We plan to generalize and extend this abstract syntax
to avoid specific assumptions and to cover all the C constructs.
In particular, we plan to use the formalization of character sets to lift the ASCII assumption.
The purpose of this abstract syntax is to support
our formal definition of (a subset of) C.
In contrast, the purpose of the more recently added abstract syntax for tools is to support the implementation of tools for C in ACL2.
Currently ATC uses the abstract syntax defined here and not that one,
but we plan to have it use that one instead,
leaving the purpose of the one defined here
exclusively to formally define the language.
Because of its current use in ATC,
the abstract syntax defined here
captures constructs both before and after preprocessing;
however, after ATC no longer uses it,
we plan to change it to capture
just the constructs after preprocessing,
and more broadly we plan to formalize
the translation phases [C:5.1.1.2] in detail.
Subtopics
- Tyspecseq
- Fixtype of type specifier sequences [C:6.7.2].
- Expr
- Fixtype of expressions [C:6.5].
- Binop
- Fixtype of binary operators [C:6.5.5-14] [C:6.5.16].
- Fileset
- Fixtype of file sets.
- Obj-declor
- Fixtype of object declarators [C:6.7.6].
- Ident
- Fixtype of identifiers [C:6.4.2].
- Iconst
- Fixtype of integer constants [C:6.4.4.1].
- Obj-adeclor
- Fixtype of abstract object declarators [C:6.7.7].
- Const
- Fixtype of constants [C:6.4.4].
- Fundef
- Fixtype of function definitions [C:6.9.1].
- Unop
- Fixtype of unary operators [C:6.5.3].
- File
- Fixtype of files.
- Tag-declon
- Fixtype of declarations of structure, union, and enumeration types
[C:6.7.2.1] [C:6.7.2.2].
- Fun-declor
- Fixtype of function declarators [C:6.7.6].
- Obj-declon
- Fixtype of object declarations [C:6.7].
- Iconst-length
- Fixtype of lengths of integer constants [C:6.4.4.1].
- Abstract-syntax-operations
- Operations on the C abstract syntax.
- Label
- Fixtype of labels of labeled statements [C:6.8.1].
- Struct-declon
- Fixtype of structure declarations [C:6.7.2.1].
- Initer
- Fixtype of initializers [C:6.7.9].
- Ext-declon
- Fixtype of external declarations [C:6.9].
- Fun-adeclor
- Fixtype of abstract function declarators [C:6.7.7].
- Expr-option
- Fixtype of optional expressions.
- Iconst-base
- Fixtype of bases of integer constants [C:6.4.4.1].
- Initer-option
- Fixtype of optional initializers.
- Iconst-option
- Fixtype of optional integer constants.
- Tyspecseq-option
- Fixtype of optional type specifier sequences.
- Stmt-option
- Fixtype of optional statements.
- Scspecseq
- Fixtype of storage class specifier sequences [C:6.7.1].
- Param-declon
- Fixtype of parameter declarations [C:6.7.6].
- Obj-declon-option
- Fixtype of optional object declarations.
- File-option
- Fixtype of optional files.
- Tyname
- Fixtype of type names [C:6.7.7].
- Transunit
- Fixtype of translation units [C:6.9].
- Fun-declon
- Fixtype of function declarations [C:6.7].
- Transunit-result
- Fixtype of errors and translation units.
- Param-declon-list
- Fixtype of lists of parameter declarations.
- Struct-declon-list
- Fixtype of lists of structure declarations.
- Expr-list
- Fixtype of lists of expressions.
- Tyspecseq-list
- Fixtype of lists of type specifier sequences.
- Ident-set
- Fixtype of sets of identifiers.
- Ident-list
- Fixtype of lists of identifiers.
- Ext-declon-list
- Fixtype of lists of external declarations.
- Unop-list
- Fixtype of lists of unary operators.
- Tyname-list
- Fixtype of lists of type names.
- Fundef-list
- Fixtype of lists of function definitions.
- Fun-declon-list
- Fixtype of lists of function declarations.
- Binop-list
- Fixtype of lists of binary operators.
- Stmt-fixtypes
- Mutually recursive fixtypes for statements (and blocks).
- Expr-fixtypes
- Mutually recursive fixtypes for expressions.
