#include <stdint.h>
#define INTPTR_MAX                                       /* FIXME */     (32767)

/*
STDC(199901)
*/