Rationale: Many programming languages (in which we would like to write high-assurance code) have support for sized integer types, and being able to use these in array parameters would be very helpful.
They seem to be supported fine using CType when not used in arrays, maybe the fix is as easy as adding CType to the param_type macro in camkes/templates/arch-definitions.thy?
Currently I'm using a workaround passing char instead of uint8_t, but the latter conveys much more cleanly what I want to express (plus char may or may not be unsigned, and unsigned char is not supported).