|
|
|---|
|
|
|
|---|
Fixtype of identifiers [C17:6.4.2].
This is a product type introduced by fty::defprod.
For now we represent C identifiers as ACL2 strings, which suffice to represent all the ASCII C identifiers. We wrap ACL2 strings into a one-field product fixtype to make it easier to modify or extend this fixtype in the future.
Unconstrained ACL2 strings may not be valid C ASCII identifiers. In the future we may extend this fixtype with suitable restrictions on the ACL2 string.
A C implementation may limit the number of significant characters in identifiers [C17:6.4.2.1/5] [C17:6.4.2.1/6] [C17:5.2.4.1], to 31 for external identifiers and 63 for internal identifiers. In the future, we may add this constraint to this fixtype.