#include <stdint.h>
#define WCHAR_MAX                                                     (0x10FFFF)

/*
STDC(199901)
*/