typedef unsigned int                                                   char32_t;

/*
STDC(201112)
*/