Dimb-paramdecl
Disambiguate a parameter declaration.
- Signature
(dimb-paramdecl paramdecl table)
→
(mv erp new-paramdecl new-table)
- Arguments
- paramdecl — Guard (paramdeclp paramdecl).
- table — Guard (dimb-tablep table).
- Returns
- new-paramdecl — Type (paramdeclp new-paramdecl).
- new-table — Type (dimb-tablep new-table).
We start by disambiguating the declaration specifiers,
which may result in extending the disambiguation table.
In valid code, the typedef storage class specifier
cannot occur among the declaration specifiers of a parameter declaration,
so we ignore the disambiguation kind returned by
the ACL2 function that processes the declaration specifiers;
when we call that function, we initialize the kind to :objfun,
and if the code is valid that will be also the returned kind.
Then we call a separate function to disambiguate the parameter declarator
(which is a notion in our abstract syntax, not in [C]);
see paramdeclor).
