ASCII identifiers in the C abstract syntax of tools.
Our abstract syntax allows identifiers to be anything, for the reasons explained in ident. Nonetheless, given our current concrete syntax definition, parsed identifiers always consist of ASCII characters satisfying certain restrictions (start with a letter, etc.). Disambiguator and validator preserve this property of identifiers. The printer currently checks, at run time, that identifiers satisfy a weaker property than this, but it should really only be used to print abstract syntax whose identifiers satisfy the stronger property that is being discussed and defined here. C-to-C transformations may intentionally break this property (see the discussion in ident), but the abstract syntax should be eventually transformed into a printable form before actually printing it.
Here we formalize the notion of ASCII identifiers, and we define predicates on the abstract syntax that check that all the identifiers satisfy this property. More precisely, we define two sets of predicates: one is for standard C, and one is for C with GCC extensions. The difference is that the letter has more keywords, and thus (finitely) fewer identifiers.