Validation-information
Information calculated and used by the validator.
The validator calculates and uses information, such as types,
and annotates the abstract syntax with some of this information.
Here we introduce fixtypes for this information,
and operations on those fixtypes.
We also introduce predicates over the abstract syntax,
to check that the annotations from the validator are present.
This is not the same as saying that the constructs are validated;
the predicates just say that information of the right type is present.
Subtopics
- Abstract-syntax-annop
- Definition of the predicates that check whether
the abstract syntax is annotated with validation information.
- Types
- C types used by the validator.
- Abstract-syntax-anno-additional-theroems
- Additional theorems about the annotation predicates.
- Valid-ext-info
- Fixtype of validation information about identifiers with external
linkage.
- Valid-table
- Fixtype of validation tables.
- Valid-ord-info
- Fixtype of validation information about ordinary identifiers.
- Uid
- Fixtype of unique identifiers.
- Stmts-types
- Types of statements and related entities,
from the validation information.
- Lifetime
- Fixtype of lifetimes.
- Initdeclor-info
- Fixtype of validation information for initializer declarators.
- Fundef-types
- Types of the values returned by a function,
from the validation information.
- Expr-type
- Type of an expression, from the validation information.
- Valid-defstatus
- Fixtype of definition statuses for validation.
- Var-info
- Fixtype of validation information for variables.
- Valid-ord-info-option
- Fixtype of
optional validation information about ordinary identifiers.
- Valid-ext-info-option
- Fixtype of optional validation information
about identifiers with external linkage.
- Uid-option
- Fixtype of optional unique identifiers.
- Linkage-option
- Fixtype of optional linkages.
- Linkage
- Fixtype of linkages.
- Lifetime-option
- Fixtype of optional lifetimes.
- Valid-table-option
- Fixtype of optional validation tables.
- Iconst-info
- Fixtype of validation information for integer constants.
- Param-declor-nonabstract-info
- Fixtype of validation information for
non-abstract parameter declarators.
- Fundef-info
- Fixtype of validation information for function definitions.
- Expr-null-pointer-constp
- Check whether an expression of a given type is potentially a null
pointer constant [C17:6.3.2.3/3].
- Valid-scope
- Fixtype of validation scopes.
- Const-expr-null-pointer-constp
- Check whether a constant expression of a given type is potentially a
null pointer constant [C17:6.3.2.3/3].
- Expr-string-info
- Fixtype of validation information for string literal expressions.
- Expr-funcall-info
- Fixtype of validation information for function call expressions.
- Expr-arrsub-info
- Fixtype of validation information for array subscript expressions.
- Tyname-info
- Fixtype of validation information for type names.
- Transunit-info
- Fixtype of validation information for translation units.
- Expr-unary-info
- Fixtype of validation information for unary expressions.
- Expr-const-info
- Fixtype of validation information for constant expressions.
- Expr-binary-info
- Fixtype of validation information for binary expressions.
- Stmt-types
- Types of a statement, from the validation information.
- Block-item-list-types
- Types of a list of block items, from the validation information.
- Initer-type
- Type of an initializer, from the validation information.
- Valid-ord-scope
- Fixtype of validation scopes of ordinary identifiers.
- Uid-increment
- Create a fresh unique identifier.
- Uid-equal
- Coerce-var-info
- Coerce a value to var-info.
- Valid-externals
- Fixtype of validation information associated with identifiers with
external linkage.
- Irr-var-info
- An irrelevant validation information for variables.
- Valid-scope-list
- Fixtype of lists of validation scopes.
- Irr-valid-table
- An irrelevant validation table.
- Irr-lifetime
- An irrelevant lifetime.
- Irr-uid
- An irrelevant unique identifier.
- Irr-linkage
- An irrelevant linkage.
- Block-item-types
- Types of a block item, from the validation information.
- Comp-stmt-types
- Types of a compound statement, from the validation information.
