|
|
|---|
|
|
|
|---|
Annotation of the C abstract syntax of tools.
Our validator adds some information (`annotations') to the abstract syntax constructs if it successfully validates them. We 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.