Unambiguity
Unambiguity of the C abstract syntax for tools.
Our abstract syntax includes ambiguous constructs,
i.e. constructs that capture syntactically ambiguous constructs;
see the documentation of the abstract syntax for details.
The disambiguator, if successful,
removes those constructs, leaving only the unambiguous ones.
Here we define predicates over the abstract syntax
that say whether the constructs are unambiguous,
i.e. there are no ambiguous constructs.
The definition is simple, just structural.
For now we do not make any checks on GCC extensions,
even though they may contain expressions.
This mirrors the treatment in the disambiguator:
the reason for this (temporary) limitation is explained there.
Besides defining the unambiguity predicates,
we also provide rules to automate guard and return proofs
that involve the unambiguity predicates.
The rules about the fixtype deconstructors
automate the guard proofs;
the rules about the fixtype constructors
automate the return proofs.
Subtopics
- Exprs/decls/stmts-unambp
- Check if expressions, declarations, and related entities
are unambiguous.
- Transunit-ensemble-unambp
- Check if a translation unit ensemble is unambiguous.
- Expr/tyname-unambp
- Check if an expression or type name is unambiguous.
- Declor/absdeclor-unambp
- Check if a declarator or abstract declarator is unambiguous.
- Decl/stmt-unambp
- Check if a declaration or statement is unambiguous.
- Fundef-unambp
- Check if a function definition is unambiguous.
- Extdecl-unambp
- Check if an external declaration is unambiguous.
- Transunit-unambp
- Check if a translation unit is unambiguous.
- Type-spec-list-unambp
- Check if a list of type specifiers is unambiguous.
- Extdecl-list-unambp
- Check if a list of external declarations is unambiguous.
- Type-spec-list-unambp-of-sublists
- Theorems saying that the sublist of type specifiers
extracted via some abstract syntax operations
is unambiguous if the initial list is unambiguous.
- Expr-unambp-of-operation-on-expr-unambp
- Preservation of unambiguity by certain operations on expressions.
- Dirabsdeclor-unambp
- Check if a direct abstract declarator is unambiguous.
- Dirabsdeclor-option-unambp
- Check if an optional direct abstract declarator is unambiguous.
- Desiniter-list-unambp
- Check if a list of initialziers with optional designations
is unambiguous.
- Strunispec-unambp
- Check if a structure or union specifier is unambiguous.
- Structdeclor-unambp
- Check if a structure declarator is unambiguous.
- Structdeclor-list-unambp
- Check if a list of structure declarators is unambiguous.
- Structdecl-unambp
- Check if a structure declaration is unambiguous.
- Structdecl-list-unambp
- Check if a list of structure declarations is unambiguous.
- Statassert-unambp
- Check if a static assertion declaration is unambiguous.
- Spec/qual-unambp
- Check if a specifier or qualifier is unambiguous.
- Spec/qual-list-unambp
- Check if a list of specifiers and qualifiers is unambiguous.
- Paramdeclor-unambp
- Check if a parameter declarator is unambiguous.
- Paramdecl-unambp
- Check if a parameter declaration is unambiguous.
- Paramdecl-list-unambp
- Check if a list parameter declarations is unambiguous.
- Member-designor-unambp
- Check if a member designator is unambiguous.
- Initer-option-unambp
- Check if an optional initializer is unambiguous.
- Initdeclor-unambp
- Check if an initializer declarator is unambiguous.
- Initdeclor-list-unambp
- Check if a list of initializer declarators is unambiguous.
- Genassoc-list-unambp
- Check if a list of generic associations is unambiguous.
- Expr-option-unambp
- Check if an optaional expression is unambiguous.
- Enumspec-unambp
- Check if an enumeration specifier is unambiguous.
- Enumer-list-unambp
- Check if a list of enumerators is unambiguous.
- Dirdeclor-unambp
- Check if a direct declarator is unambiguous.
- Desiniter-unambp
- Check if an initializer with optional designations is unambiguous.
- Designor-list-unambp
- Check if a list of designators is unambiguous.
- Declspec-unambp
- Check if a declaration specifier is unambiguous.
- Declspec-list-unambp
- Check if a list of declaration specifiers is unambiguous.
- Declor-option-unambp
- Check if an optional declarator is unambiguous.
- Const-expr-option-unambp
- Check if an optional constant expression is unambiguous.
- Block-item-list-unambp
- Check if a list of block items is unambiguous.
- Align-spec-unambp
- Check if an alignment specifier is unambiguous.
- Absdeclor-unambp
- Check if an abstract declarator is unambiguous.
- Absdeclor-option-unambp
- Check if an optional abstract declarator is unambiguous.
- Type-spec-unambp
- Check if a type specifier is unambiguous.
- Tyname-unambp
- Check if a type name is unambiguous.
- Stmt-unambp
- Check if a statement is unambiguous.
- Label-unambp
- Check if a label is unambiguous.
- Initer-unambp
- Check if an initializer is unambiguous.
- Genassoc-unambp
- Check if a generic association is unambiguous.
- Expr-unambp
- Check if an expression is unambiguous.
- Expr-list-unambp
- Check if a list of expressions is unambiguous.
- Enumer-unambp
- Check if an enumerator is unambiguous.
- Designor-unambp
- Check if a designator is unambiguous.
- Declor-unambp
- Check if a declarator is unambiguous.
- Decl-unambp
- Check if a declaration is unambiguous.
- Decl-list-unambp
- Check if a list of declarations is unambiguous.
- Const-expr-unambp
- Check if a constant expression is unambiguous.
- Block-item-unambp
- Check if a block item is unambiguous.