#include <stdint.h>
#define UINTPTR_MAX                                 /* FIXME */          (65535)

/*
STDC(199901)
*/